 \documentclass{fac}

\usepackage{amsmath,amssymb,wasysym,xspace}
\usepackage{mathptmx,stmaryrd}
\usepackage{eurosym}
\usepackage[T1]{fontenc}
\usepackage[mathscr]{euscript}
\usepackage[usenames,dvipsnames]{color}
\usepackage{epsfig}
\usepackage{amsfonts}
\usepackage{latexsym}
\usepackage{mathpartir}
\usepackage{listings}
\usepackage{enumerate}
\usepackage{url}
\usepackage{hyperref}
\usepackage{wasysym}


\usepackage{hyperref}
\usepackage{proof}
\usepackage{macron}
\usepackage{typecasemacro}

\newenvironment{rcases}
  {\left\lbrace\begin{aligned}}
  {\end{aligned}\right\rbrace}
  
\usepackage{lineno}
\newtheorem{mydef}{Definition}[section]
\newtheorem{myexamp}[mydef]{Example}%[section]
\newtheorem{mytheo}[mydef]{Theorem}%[section]
\newtheorem{myremark}[mydef]{Remark}%[section]
\newtheorem{mylemma}[mydef]{Lemma}%[section]
\newtheorem{newnotation}[mydef]{Notation}%[section]
\newtheorem{proposition}[mydef]{Proposition}%[section]
%  \newenvironment{mydef              {\begin{definition}}{\end{definition}}





%\input{macros}

\title[Event-Based %Approach   
Runtime Adaptation in Communication-Centric Systems - Revision of \today]{%An Event-Based Approach to \\
Event-Based 
Runtime Adaptation in Communication-Centric Systems
}
\author[C. Di Giusto J.A. P\'{e}rez]
{Cinzia Di Giusto$^1$ and
Jorge A. P\'{e}rez$^2$\\
$^1$
Universit\'{e} de Nice Sophia-Antipolis, CNRS, I3S, UMR 7271, Sophia Antipolis (FR) \\
$^2$Johann Bernoulli Institute for Mathematics and Computer Science, University of Groningen (NL)
}

\correspond{Jorge A. P\'{e}rez,
%JBI,
%University of Groningen, (The Netherlands).
 e-mail: j.a.perez@rug.nl}

\pubyear{2015}
\pagerange{\pageref{firstpage}--\pageref{lastpage}}


\begin{document}
\label{firstpage}

\makecorrespond

%
\maketitle

\begin{abstract}
We use the term 
\emph{communication-centric systems} to refer to 
software systems 
built as assemblies of distributed ar\-ti\-facts
that interact following predefined structured  protocols. 
\emph{Session-based concurrency} 
is a type-based approach to
ensure conformance of communication-centric systems to such protocols.
This paper presents a model of 
{session-based concurrency}
with mechanisms for \emph{runtime adaptation}. 
Thus, our model allows us to specify com\-mu\-ni\-ca\-tion-centric systems 
whose session behavior can be dynamically updated at runtime.
We propose an \emph{event-based} approach: 
adaptation requests,
issued by the system itself or by its context,
 are assimilated to events
which may trigger runtime adaptation routines.
 These  routines exploit type-directed checks to 
  enable the reconfiguration of processes with active sessions.
We develop a 
 type system that ensures \emph{communication safety} 
and \emph{consistency} properties:
while the former guarantees
absence of runtime communication errors, 
the latter ensures that update actions  do not disrupt already established sessions.
We provide soundness results for structured protocols in binary and multiparty settings.
\end{abstract}

\begin{keywords}
behavioral types,
session types, 
runtime adaptation,
process calculi.
\end{keywords}

\section{Introduction}\label{s:intro}
%\noindent{\textit{\textbf{Context.}}}
Modern software
systems are built as assemblies of distributed, heterogeneous ar\-ti\-facts
whose interactions follow predefined communication protocols.
As a consequence, correctness in these \emph{com\-mu\-ni\-ca\-tion-centric} systems
largely depends on ensuring that such dialogues are consistent.
\emph{Session-based concurrency} is a type-based approach to
ensure conformance of dialogues to prescribed protocols:
dialogues are organized into %basic
units called \emph{sessions}; interaction patterns are abstracted as \emph{session types}~\cite{DBLP:conf/esop/HondaVK98},
against which specifications may be checked. %\looseness=-1
As these specifications are often given in the $\pi$-calculus~\cite{DBLP:journals/iandc/MilnerPW92a,DBLP:conf/esop/HondaVK98},
protocol conformance can be analyzed at the level of concurrent processes.

Communication-centric systems %typically %open, and
operate on open and dynamic infrastructures; in such scenarios, 
\emph{runtime adaptation} appears as an indispensable feature to ensure 
flexible and uninterrupted system operation.
Here we understand runtime adaptation as the dynamic modification 
(or reconfiguration)
of a system's behavior in response to an exceptional event, 
such as, e.g., a varying requirement or a local failure.
These events are 
not necessarily catastrophic but are hard to predict.
In this context, 
conformance to structured protocols and
%dynamic reconfiguration 
runtime adaptation
appear as intertwined concerns:
although
the specification of runtime adaptation is
not strictly tied to that of structured protocols,
steps of 
%dynamic reconfiguration 
runtime adaptation
have a direct influence in a system's interactive behavior and overall correctness.

We are interested in integrating forms of
%We address the integration of mechanisms 
runtime adaptation
into models of %a model of
session-based concurrency.
This integration concerns extending models of session-based concurrency with useful forms of adaptation,
but also equipping such extended models with appropriate analysis techniques for protocol conformance.

As a first answer to this challenge, in previous work~\cite{GiustoP14short} we
extended a typed process framework 
for binary sessions
with constructs from the model of \emph{adaptable processes}~\cite{BGPZLMCS}.
Such a model relies on \emph{locations} as explicit delimiters for 
process behavior:
these are transparent, possibly nested computation sites.
There are two key constructs:
\begin{enumerate}[$\bullet$]
\item Given a  process $P$,
the \emph{located process} $\scomponent{\locf{loc}}{P}$ denotes the fact that $P$ resides in location \locf{loc}.
Transparency of locations enables $P$ to interact with processes outside \locf{loc}.

% (or, alternatively, that $P$ has scope $\locf{loc}$).
%We use locations as explicit delimiters for runtime adaptation steps:
\item An \emph{update process} $\nadapt{\locf{loc}}{U}$ specifies that the behavior currently enclosed by
location 
\locf{loc}
should be modified according to 
the \emph{adaptation routine}
$U$ (which is, intuitively, a function from processes to processes located  at \locf{loc}).
\end{enumerate}
Located processes allow us to specify distributed topologies of interacting processes; 
since locations may enclose a process implementing
one or more sessions, update processes allow us to express rich adaptation routines.
At the operational level, located and update processes are complementary: 
a located process and an update process on the same location 
are expected to synchronize in order to formally realize an adaptation step.
The result of this synchronization is a located process whose behavior depends on the adaptation routine.
More concretely, 
given $\scomponent{\locf{loc}}{P}$ and $\nadapt{\locf{loc}}{U}$, we intuitively have that $U$
``moves'' to 
the context of the located process and is ``applied to'' $P$.
(The exact operational semantics that justifies this synchronization is illustrated later on.)

We would like to guarantee that adaptation steps resulting from the synchronization of located and update processes
 preserve overall system correctness.
 In a session-typed setting 
 this entails ensuring that such synchronizations do not jeopardize session protocols enclosed by locations. 
As a  very simple example of a dangerous adaptation routine, consider 
the update process 
$\nadapt{\locf{loc}}{\mathbf{0}}$:
as it will be formalized later on, 
this update process decrees that 
the new behavior at $\locf{loc}$ should be the inactive process, without any considerations 
on the current behavior.
As such, it would discard any established session protocols and 
compromise any conceivable form of protocol conformance; 
processes depending on the sessions implemented at $\locf{loc}$ would lack complementary partners.
To rule out adaptation steps that jeopardize established protocols, 
communication and adaptation actions should be harmonized.
To this end, in~\cite{GiustoP14short} we defined the notion of \emph{consistency}, according to which 
a located process can be updated only if it does not contain active (established) session protocols. 
Adaptation actions are enabled only for locations that do not enclose running sessions; 
an associated type system ensures 
protocol conformance but also 
that session protocols are never disrupted as a result of an adaptation step.
This is a simple solution that 
privileges communication over adaptation, 
in the sense that adaptation is enabled only when sessions in a location are in a quiescent state.
In applications, however, it may be necessary to give communication and adaptation
 a similar status, enabling adaptation steps also on locations that contain already established sessions. 
 The main contribution of this paper is a session-typed framework that 
enables this kind of adaptation steps, thus 
extending the applicability and expressiveness of the approach introduced in~\cite{GiustoP14short}.

We briefly motivate our approach.
Let   $\ST, \STT, \ldots$ denote session types; also, let 
$x, y, \ldots, $ and 
%$\cha^p, \kappa_1^q \ldots$ 
$k, k', \ldots$
denote channel variables and  session channels, respectively.
We propose novel update processes in which 
the adaptation routine $U$  
dynamically checks
the current state of the
session protocols running in \locf{loc}.
In their simplest form, these novel update processes
concern only one session channel and are of the form:
%are written
\begin{equation}
%{\nadaptbig{\locf{loc}}{\mycase{{x}}{{x_{}^{}{:}\STT_{}^{i}}}{U_i}{}}}
\nadaptbig{\locf{loc}}{\mycaseni{x}{(\STT_1:U_1), \cdots, (\STT_m:U_m)}} \qquad (m \geq 1)
\label{eq:sec10}
\end{equation}
where 
$x$ denotes a channel variable,
$\STT_1, \ldots, \STT_m$  
are session types, and $U_1, \ldots, U_m$ are processes in which $x$ occurs free.
This \emph{typeful} update process  may be better  introduced by considering 
its interaction with a located process
$\scomponentbig{\locf{loc}}{ Q} $
in which $Q$ implements a session of type $\ST$ along channel $k$:
If there is a  $j \in \{1, .., m\}$ such that
 types $\ST$ and $\STT^j$ ``match'' (up to session subtyping~\cite{DBLP:journals/acta/GayH05}), 
 %(roughly $\STT^j$ is a subtype of $\ST$)
then
the located process is updated to 
$\scomponentbig{\locf{loc}}{U_j\subst{k}{x}}$, in which channel $k$ is used to 
instantiate the alternative $U_j$.
Otherwise, if no $\STT^j$ validates a match, then 
the located process is kept unchanged and the update process is consumed.
The formal operational semantics for these typeful update processes exploits the 
constructs for 
\emph{dynamic type inspection}, 
as put forward by Kouzapas et al.~\cite{KouzapasJ13,Kouzapas12}.

%The
%integration of runtime adaptation into sessions %-based concurrency
%is delicate, and involves
%defining 
%not only \emph{what} should be the  state of the system after an adaptation step but also 
%\emph{when} such a step should be triggered.
%Update processes enable us to specify the ``what''; 
%in order to specify the ``when'', we advocate an \emph{event-based} approach:
%we consider constructs for issuing and handling \emph{adaptation requests}, 
%which can be either internal or external to the location and can be naturally assimilated to events.

%Update processes rely on the protocol state at a given location to assess the suitability of adaptation routines.
%Our semantics for update relies on
%(a)~\emph{monitors} which store the current type for each running session; and
%(b)~a type-directed test on the monitors
%enclosed in a given location.
%This test % as a %actually corresponds to
%generalizes the $\mathtt{typecase}$ construct in~\cite{Kouzapas12}.

%\paragraph{\textbf{Event-Based Adaptation.}}
While expressive,
%Defined at the level of locations,
our typeful update processes %thus offer a flexible and expressive mechanism for runtime adaptation.
by themselves %, however, these processes
do not specify \emph{when} adaptation should be available.
Even though update processes could be embedded within session communication prefixes (thus creating causal dependencies between communication and adaptation),
such a specification style would only allow to handle exceptional conditions which can be fully characterized in advance.
Other exceptional conditions, in particular contextual/unsolicited runtime conditions, are much harder to express by interleaving update processes
within structured protocols.

To offer a uniform solution to this issue,
we propose an \emph{event-based} approach
to trigger update processes.
We endow each location with a \emph{queue} of adaptation requests;
such requests
may be internal or external to the location.
%In our example, an external request could be, e.g.,
%%a signal from the infrastructure on which both partners are deployed, or
%a warning message from the buyer's bank indicating that an exchange with the bank is required before committing to the purchase with the seller.
Location queues are independent from session behavior, and 
their identity is visible to processes.
These queues are intended as interfaces between the process enclosed by 
the location and their context.
%This way, e.g., the queue of location \locf{seller} becomes the only way in which its surrounding context may only influence the communication behavior.
To issue an adaptation request $r$ for location $\locf{loc}$, our process syntax includes \emph{adaptation signals}, written $\outC{\locf{loc}}{r}$.
%where $r$ stands for an adaptation request.
Similar to ordinary communication prefixes, 
these signals are also independent from sessions.
% processes such as $P_x$ and $Q_y$ may issue adaptation requests.
Then, 
we may
detect the presence of %message
request $r$ in the queue of %location
\locf{loc}
using the \emph{arrival predicate} $\arrive{\locf{loc}, r}$~\cite{Kouzapas12}.
As a simple example, let $\mathtt{upd}_E$ denote  an \emph{external} adaptation request.
The process 
%\begin{equation}
\[
\mu \rv{X}.\ifte{\arrive{\locf{loc}, \mathtt{upd}_E}}{\nadaptbig{\locf{loc}}{U}}{\rv{X}}
\]
%\end{equation}
combines arrival predicates, conditional expressions, and recursion to 
express a persistent, event-based adaptation policy that  
continuously checks for the arrival of an external request  to the queue of location 
\locf{loc}. If such a request is detected then the update process $\nadaptbig{\locf{loc}}{U}$ is 
triggered; otherwise, the policy is spawned again. 



%Process $U^*_{xy}$ . As soon as such a request is detected update process $U_{xy}$ will be triggered.

Summing up, our process model for session-based concurrency and runtime adaptation 
 includes four key constructs: located processes, type-directed update processes, 
adaptation signals, and location queues. 
While the first construct is inherited from 
our previous work~\cite{GiustoP14short}, 
our update processes enhance those in~\cite{GiustoP14short} using type-directed checks.
Also, adaptation signals and location queues for event-based  adaptation are new to this presentation.
This model is then coupled 
with a session type system
that ensures the following key properties:
\begin{enumerate}[$\bullet$]
\item \textbf{\emph{Safety}}: well-typed programs do not exhibit communication errors (e.g., mismatched messages).
\item \textbf{\emph{Consistency}}: well-typed programs do not allow adaptation actions that disrupt already established sessions.
\end{enumerate}
On the one hand, 
safety is the typical guarantee expected from any session type discipline, here considered in a rich setting that combines session communication with runtime adaptation. On the other hand, consistency is a guarantee unique to our setting: it relates the behavior of the adaptation mechanisms with the preservation of prescribed typed interfaces.
We show that well-typed programs are safe and consistent (Theorems~\ref{t:safety} and~\ref{t:multisafety}): this ensures that specified session protocols are respected, while forbidding incautious adaptation steps that could disrupt the session behavior of interacting partners.

In the first part of the paper we consider a process model and an associated type system for \emph{binary sessions}, as our goal is to motivate and develop our approach for event-based adaptation in a simple but representative setting. 
%However, 
Nevertheless, 
the key ingredients of our approach 
are sufficiently simple and general so as to  be casted in a setting for \emph{multiparty communications}.
In the second part of the paper, as a proof of concept, we 
describe a generalization of our 
 event-based approach to  multiparty, asynchronous communication.

Our generalization to multiparty communication 
builds upon the framework developed by Coppo et al.~\cite{CDV15j}.
Such a framework uses global types (or \emph{choreographies}) and \emph{monitored processes} as main  ingredients.
A global type  abstracts an overall sequence of communications between two or more participants. 
By projecting a global type onto each participant, one obtains  
a series of \emph{local types}, one for each communication partner. In~\cite{CDV15j}, such local types are used as \emph{monitors} for the processes that implement each partner: a monitor contains participant information, and enables the visible actions of the process. 
The association  of a monitor and a process is called a \emph{monitored process}; a process is itself typed, and the relation between a process type and the monitor is given by a so-called \emph{adequacy relation}. 
The implementation of the whole choreography is given as a collection of monitored processes, or \emph{network}.
By considering a network together with a global state, one then obtains a  \emph{system}.
This approach ensures a desirable separation between the global type, the monitors (local types), and the processes themselves. 
Adaptation is specified at the level of global types, as their 
syntax includes an explicit signal (called \emph{flag}) that defines a form of \emph{anticipated adaptation} between all participants of the choreography.
As a result of this coordinated signal, an (unspecified) adaptation function determines a new choreography for the system, relying on the global state. Based on such a choreography, new implementations for all partners are determined exploiting a centralized repository of typed processes, called \emph{collection}.

In our proof of concept, we include typeful update processes and eventful constructs into the framework of~\cite{CDV15j}.
As a result, we obtain an alternative framework 
 in which adaptation is not specified at level of types, and is based on events that handle internal and external adaptation requests.
In fact, our  global types do not consider adaptation flags; 
rather, in order to express internal adaptation requests, we equip processes with an explicit output message whose communication object denotes a choreography. 
This message can be accessed by all protocol participants (using the shared queue) so to determine their updated behavior. 
Moreover, networks in our model are distributed collections of locations, each containing a monitored process,  a local collection of processes, and a queue. 
This queue is useful to model external adaptation requests targeted to a particular protocol participant. Such requests can be of two forms: they may either upgrade a process in the local collection or update the participant's current implementation using a type-directed check, following the update processes introduced for binary sessions (cf. actually, it corresponds to process~\eqref{eq:sec10} above). As a result, we obtain a setting in which internal adaptation is no longer anticipated at the level of types and concerns all participants of the choreography, while extern  an adaptation request focuses on a single participant. We show that this variant of the framework in~\cite{CDV15j} also enjoys safety and consistency properties (Theorem~\ref{t:multisafety}). 


%\paragraph
%\noindent{\textbf{Organization.}}
\paragraph{Contributions and Organization.}
The rest of the paper is organized as follows:
\begin{enumerate}[$-$]
\item Next,
we illustrate 
session-based concurrency, 
our approach and contributions using by means of examples (\S\,\ref{s:overv}).
\item \S\,\ref{s:evadap} presents our process model of binary sessions  with  constructs for 
%event-based 
runtime adaptation. Then, \S\,\ref{s:types} presents our
session type system, which ensures safety and consistency for processes with adaptation mechanisms
(Theorem~\ref{t:safety}).
%In \S\,\ref{s:compart} we discuss a process model of communication and adaptation  with explicit compartments; it distills the main features of the model in \S\,\ref{s:evadap}.
\item In \S\,\ref{s:multi} we describe the generalization of our approach to multiparty communications, defined as a
variant of the framework given in~\cite{CDV15j}.
We show communication safety and consistency of adaptation steps
(Theorem~\ref{t:multisafety}).
\item At the end, we discuss related works~(\S\,\ref{s:relw}) 
and draw some concluding remarks~(\S\,\ref{s:concl}).
\end{enumerate}
The appendix collects omitted definitions and proofs.

This paper is an extended and revised version of the workshop paper~\cite{GiustoP14event}.
The current presentation offers additional explanations and proofs of technical results. 
In particular, the extension of our approach to the multiparty case, given in \S\,\ref{s:multi}, is a new contribution in  this paper. 


\section{Our Approach, By Example}\label{s:overv}
In this section we illustrate our approach and contributions by means of an example, the \emph{buyer-seller protocol}.

\subsection{Binary Sessions}
In  \S\,\ref{s:evadap} and \S\,\ref{s:types}, we consider binary session types, as defined in~\cite{DBLP:conf/esop/HondaVK98}:
$$
\begin{array}{rll}
\ST, \STT ::= & ?(T).\STT   & \text{input a value of type $T$, continue as $\STT$}\\ 
\sep &  !(T).\STT & \text{output a value of type $T$, continue as $\STT$}\\ 
       \sep & \&\{n_1{:}\ST_1, \cdots,  n_m{:}\ST_m \} \qquad & \text{branching (external choice)} \\
         \sep &  \oplus\{n_1{:}\ST_1, \cdots,  n_m{:}\ST_m \} & \text{selection (internal choice)} \\
   \sep &   \mu t.\ST  \sep t   &  \text{recursive session} \\
  \sep & \tend & \text{terminated session}
   \end{array}
$$
%As an example, 
%We 
where $T$ stands for both basic types (e.g., booleans, integers) and session types $\ST$.
Also, $n_1, \ldots, n_m$ denote \emph{labels}.
To illustrate session types 
%and motivate our contributions using an example.
consider
%the %structured
%interaction of
two participants, 
a buyer \pt{B} and a seller \pt{S}, which interact as follows. % the protocol given next. % following the protocol.
First, \pt{B} sends to \pt{S} the name of an item and \pt{S} replies back with its price.
Then, depending on the amount, \pt{B} either adds the item to its shopping cart or closes the transaction.
In the latter case the protocol ends.
In the former case \pt{B} must further choose a paying method. % and the transaction ends.
From \pt{B}'s perspective, this protocol may be described by
the session type 
$$\ST_{\mathtt{buy}} = \,\,!\mathsf{item}.\,?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$$ where
$\mathsf{item}$ and $\mathsf{amnt}$ are base types and
%$\ST_{\mathtt{pay}}$ is %defined as
%\begin{equation*}
$$
\ST_{\mathtt{pay}} \,=\,\oplus\{\mathtt{addItem}:\, \oplus\{\mathtt{ccard}:\, \ST_\mathtt{cc} \,,\, \mathtt{payp}:\, \ST_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \}.
$$
%\end{equation*}
%In the syntax of session types,
%Above `$.$' denotes sequential composition, $!$ and $?$ stand for output and input, %respectively,
%and $\tend$ stands for the empty protocol.
Thus, 
session type $\ST_{\mathtt{buy}}$ says that protocol
 $\ST_{\mathtt{pay}}$ may only be enabled after sending a
value of type $\mathsf{item}$ and receiving a value of type $\mathsf{amnt}$.
Also,
$\mathtt{addItem}$, $\mathtt{ccard}$, $\mathtt{cc}$, and $\mathtt{payp}$ denote labels
in the internal choice.
%completed protocol. CINZIA: I think that the word completed can be misleading here
%In $\ST_{\mathtt{pay}}$,
%Session
Types
%we write
$\ST_\mathtt{cc}$ and $\ST_\mathtt{pp}$ denote the behavior of each payment method.
Following the protocol abstracted by $\ST_{\mathtt{buy}}$,
code for
\pt{B} may be specified as a $\pi$-calculus process.
Processes $P$ and $R$ below give
two specifications for \pt{B}:
\begin{eqnarray*}
P & = & \outC{x}{\mathsf{book}}.\inC{x}{a}.\ifte{a < 50}{\select{x}{\mathtt{addItem}};\select{x}{\mathtt{ccard}};P^{\mathsf{c}}}{\select{x}{\mathtt{cancel}};\mathbf{0}} \\
R & = & \outC{x}{\mathsf{game}}.\inC{x}{b}.\ifte{b < 80}{\select{x}{\mathtt{addItem}};\select{x}{\mathtt{payp}};R^{\mathsf{p}}}{\select{x}{\mathtt{cancel}};\mathbf{0}}
\end{eqnarray*}
Thus, although both $P$ and $R$ implement $\ST_{\mathtt{buy}}$,
their behavior is rather different, for they purchase different items using different payment methods (which are abstracted by processes $P^{\mathsf{c}}$ and $R^{\mathsf{p}}$).
Let us now analyze the situation for the seller $\pt{S}$.
To ensure protocol compatibility and absence of communication errors,
%$\STT$,
the session type for \pt{S}, denoted $\STT_{\mathtt{sel}}$,
should be \emph{dual} to $\ST_{\mathtt{buy}}$. This is denoted $\ST_{\mathtt{buy}} \cdual \STT_{\mathtt{sel}}$ and formalized in Definition~\ref{d:subt}.
Intuitively, duality decrees that
%That is,
every action from \pt{B} must be matched by a complementary action from \pt{S}, e.g., every output of a string in $\ST_{\mathtt{buy}}$ is matched by an input of a string in~$\STT_{\mathtt{sel}}$.
Thus, in our example, we let $\STT_{\mathtt{sel}} = \,\,?\mathsf{item}.\,!\mathsf{amnt}.\,\STT_{\mathtt{pay}}$, where
 $\STT_{\mathtt{pay}}$ and a process implementation $Q$ for \pt{S} are as follows:
\begin{eqnarray*}
\STT_{\mathtt{sel}} & = & \&\{\mathtt{addItem}:\, \&\{\mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} \\
Q & = & \inC{y}{i}.\outC{y}{price(i)}.\branch{y}{\mathtt{addItem} : \branch{y}{\mathtt{ccard}: Q^{\mathtt{c}} \alte \mathtt{ppal}: Q^{\mathsf{p}}} \alte \mathtt{cancel}: \mathbf{0}}
\end{eqnarray*}
where
%$\&$ is the type for external choice, dual to $\oplus$, and 
$price$ stands for an auxiliary function. % from $\mathsf{item}$ to $\mathsf{amnt}$.
Also, %types
$\STT_{\mathtt{cc}}$ and $\STT_{\mathtt{pp}}$ are the duals of $\ST_{\mathtt{cc}}$ and $\ST_{\mathtt{pp}}$; they are realized by processes
$Q_y^{\mathsf{c}}$ and $Q_y^{\mathsf{p}}$. %, respectively.
%$\STT_{\mathtt{cc}}$ and $\STT_{\mathtt{pp}}$ (the duals of $\ST_{\mathtt{cc}}$ and $\ST_{\mathtt{pp}}$).

The interaction of $P$ and $Q$ is defined using %in session-based concurrency 
\emph{session initialization} constructs: process
$\nopenr{u}{x{:}\ST}.P$ denotes the \emph{request} of a session of type $\ST$;
dually, $\nopena{u}{x{:}\ST}.P$ denotes the \emph{acceptance} of a session of type $\ST$.
In both cases, $u$ denotes a \emph{(shared) name} used for synchronization. 
In our example, we may have 
\begin{equation}
%\begin{eqnarray}
Sys  =   \nopenr{u}{x:\ST_{\mathtt{buy}}}.P \para \nopena{u}{y:\STT_{\mathtt{sel}}}.Q 
  \pired   \restr{\cha}{(P\subst{\cha^+}{x} \para Q\subst{\cha^-}{y})} = S' \label{eq:sec20}
%\end{eqnarray*}
\end{equation}
Thus, upon synchronization on $u$,
a new session $\cha$ is established.
Intuitively,
in process $S'$  
session $\cha$ is ``split'' into two \emph{session channels} (or \emph{endpoints}) $\cha^+$ and $\cha^-$: we write $+$ and $-$ to
denote their opposing \emph{polarities}~\cite{DBLP:journals/acta/GayH05}, which make their complementarity manifest.
The use of restriction
$\restr{\cha}$ covers both channels, thus
ensuring an interference-free medium for executing the session protocols described by $\ST$ and $\STT$.

\paragraph{Our Approach.}
We are interested in 
%In this context, the challenge of runtime adaptation consists in 
 ways of expressing and reasoning about the dynamic modification of session-typed processes such as $P$ and $Q$ above. 
  Such modifications may be desirable to 
  react to exceptional runtime conditions (say, an error) or to 
  implement new requirements. For instance, the type below defines a new payment method for \pt{S}:
  \begin{equation*}
\STT_{\mathtt{gift}} \,=\,\&\{\mathtt{addItem}:\, \&\{\mathtt{giftc}:\, \STT_\mathtt{gc} \,,\, \mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} 
\end{equation*}
Intuitively, $\STT_{\mathtt{gift}}$ \emph{extends} $\STT_{\mathtt{pay}}$ with a new alternative on label $\mathtt{giftc}$.
As such,  it is safe to use a process implementing  $\STT_{\mathtt{gift}}$  wherever a process implementing 
 $\STT_{\mathtt{pay}}$ is required.
 The \emph{safe substitution} principle that connects $\STT_{\mathtt{gift}}$  and  $\STT_{\mathtt{pay}}$ is formalized by a \emph{subtyping} relation on session types~\cite{DBLP:journals/acta/GayH05}, denoted $\csub$ (cf. Definition~\ref{d:subt}). 
This way, e.g.,  we have $\STT_{\mathtt{pay}} \csub \STT_{\mathtt{gift}}$. 
Continuing our example, let $S''$ be the process resulting from $S'$ (cf. \eqref{eq:sec20} above), after the first step stipulated by $\ST_{\mathtt{buy}}$ and $\STT_{\mathtt{pay}}$ (i.e., an exchange of a value of type $\mathsf{item}$).
Intuitively, at that point, the buyer part of $S'$ will have session type $?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$, whereas the
seller part of $S'$ will have session type $!\mathsf{amnt}.\,\STT_{\mathtt{pay}}$.
Suppose we wish to modify at runtime the part of $S''$ realizing the buyer behavior.
To preserve protocol correctness,
a candidate new implementation must conform, up to $\csub$, to the type
$?\mathsf{amnt}.\,\ST_{\mathtt{pay}}$;  a process realizing
any other type will fail to safely interact with the part of $S''$  implementing the seller.

Up to here we have considered standard $\pi$-calculus processes. Let us illustrate how located and update processes could be used in the buyer-seller scenario. 
As a simple example, 
process
\begin{equation}
W = \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST_{\mathtt{buy}}}.P} \para \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT_{\mathtt{sel}}}.Q} \,}
\label{eq:intro1}
\end{equation}
represents an explicitly distributed variant of $Sys$ given in \eqref{eq:sec20}:
the two partners now reside in different locations, namely \locf{buyer} and \locf{seller}; location \locf{sys} encloses the whole system. As a corresponding update process, %For instance,
the process below defines
a runtime update which depends on the current state of the two channels at location $\locf{sys}$:
%\begin{equation}
%R_{xy} = {\nadaptbig{\locf{sys}}{\mycase{{x,y}}{x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}}{\scomponent{\locf{buyer}}{ P'_x} \para \scomponent{\locf{seller}}{ Q'_y}}{}}} \label{eq:intro}
%\end{equation}
\begin{equation}
U_{\mathtt{bs}} = {\nadaptbigg{\locf{sys}\,}{
\mathsf{case}~x,y~ \mathsf{of}
\begin{rcases}
(\ST_{\mathtt{buy}} \,;\,  \STT_{\mathtt{sel}}) & : \scomponent{\locf{buyer}}{R} \para \scomponent{\locf{seller}}{Q} \\
(\ST^{}_{\mathtt{pay}} \,;\,  \STT^{}_{\mathtt{pay}}) & : \scomponent{\locf{buyer}}{ P^*} \para \scomponent{\locf{seller}}{ Q^*}
\end{rcases}
}} \label{eq:intro}
\end{equation}
Intuitively, %
process
$U_{\mathtt{bs}}$ %is an update process with only one alternative.
defines two possibilities for runtime adaptation.
%There are two possibilities for update which depend on the protocol state.
If the protocol has just been established 
(i.e., the current types for the two channels at \locf{sys} are $\ST_{\mathtt{buy}}$ and $\STT_{\mathtt{sel}}$) then only the buyer is updated---its new behavior will be given by process $R$ above.
If both item and price information have been already exchanged 
(i.e., the current types for the two channels at \locf{sys} are $\ST_{\mathtt{pay}}$ and $\STT_{\mathtt{pay}}$)
then new  implementations $P^*$ and $Q^*$ are installed in the respective locations.
Types are used to guide in update processes, but also to ensure that the ensuing behavior is sound. 
In the particular case of process $U_{\mathtt{bs}}$, the type system we develop in \S\,\ref{s:types} would ensure that 
process $\scomponent{\locf{buyer}}{R} \para \scomponent{\locf{seller}}{Q}$ has exactly two free session channels 
$x$ and $y$, with session types $\ST_{\mathtt{buy}}$ and $\STT_{\mathtt{sel}}$, respectively.

As a simple example of the event-based constructs, we may consider a simple variant of the process given in the Introduction, which defines a conditional adaptation policy:
\begin{equation}
P = \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{U_{\mathtt{bs}}}{\rv{X}}
 \label{eq:intro2}
\end{equation}
We write $r, r', r_0, r_1, \ldots$ to range over adaptation messages. 
Intuitively, the process in \eqref{eq:intro2} persistently checks if an adaptation message $\mathtt{upd}_E$ has arrived to the queue of location $\locf{sys}$, which we denote 
$\que{\locf{sys}}{\til{r}}$. 
Notice that such a message may be issued by process $W$ itself  or by its context, using an adaptation signal (denoted $\outC{\locf{loc}}{\mathtt{upd}_E}$).
We therefore envision systems in which communication actions, adaptation policies, and event-based constructs concurrently intact. In our example, we could have the process
\begin{equation}
W \para P \para \que{\locf{sys}}{r_0 \cdot \til{r}}
\end{equation}
which could trigger the adaptation of location $\locf{sys}$ if $r_0 = \mathtt{upd}_E$ as specified by $P$; otherwise, communication within $W$ would take place.


\subsection{Multyparty Sessions}\label{ss:multisumm}
\input{multiexample}

\section{The Process Model: Syntax and Semantics for Binary Sessions}\label{s:evadap}
%ADD POINTERS TO TYPES (duality, subtyping)


\begin{table}%[t!]
$$
\begin{array}{lrlr}
e & ::= & v \sepr x, y, z  \sepr k = k \sepr a = a & \text{expressions}  \\
  & \sepr & \arrive{\locf{loc}, r} & \text{arrival predicate} \\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  ~~\sepr~~ \nopena{u}{x:\ST}.P & \text{request / acceptance}	 \\
	& \sepr &  \outC{k}{e}.P  ~~\,\sepr~~ \inC{k}{x}.P  & \text{data output /input } \\
	&\sepr&   \select{k}{n};P ~~\!\sepr~~   \branch{k}{n_i{:}P_i}_{i \in I} & \text{selection / branching} \\
    &\sepr&   \mu \rv{X}.P ~\,\sepr~~  \rv{X} & \text{recursion / rec. variable}  \\
  	& \sepr &   P \para  P    & \text{parallel composition} \\	 
	&\sepr&   \restr{\cha}{P} ~\sepr~~ \restr{u}{P} & \text{channel / name hiding}	\\
	&\sepr&    \ifte{e}{P_1}{P_2} & \text{ conditional}	\\
	&\sepr&   \que{k}{\ST}  & \text{session monitor}  \\ 
	&\sepr&    \close{k}.P& \text{session closure}	 \\
	&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process}  \\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{x_1, \ldots,x_m}{\STT_{1}^{i}; \cdots ;\STT_{m}^{i}}{Q_i}{i \in I}} \quad& \text{update process} \\
	&\sepr&   \outC{\locf{loc}}{r}   & \text{adaptation signal}  \\
	&\sepr&   \que{\locf{loc}}{\til{r}} & \text{location queue} \\
	&\sepr&   \mathbf{0}  & \text{inaction} 
\end{array} 
$$
\caption{Process Syntax. %Session Processes with Runtime Adaptation: Syntax.
Above, annotation $\ST$ denotes a session type. % (cf. Def.~\ref{d:types})
} \label{tab:syntax}
%\vspace{-2mm}
\end{table}


%TO DO: mention abbreviations (branching), notation for labels and locations, and close process, annotations for service requests, location messages.

%Our process language of sessions with runtime adaptation
%%In a nutshell, it which 
%combines the synchronous $\pi$-calculus 
%that we have considered in~\cite{DBLP:conf/sac/GiustoP13} with constructs from the eventful session framework in~\cite{Kouzapas12}. 
%%We  also give an operational semantics for processes \\
%%, and illustrate its use with a simple example. \\

%\noindent{\bf Syntax.~}
\paragraph{\textbf{Syntax.}}
We %consider the following 
rely on 
base sets for  
\emph{names}, ranged over by $u, a, b \ldots$; 
\emph{(session) channels}, ranged over by $k, \cha^p, \ldots$, with \emph{polarity} $p \in \{+,-\}$;
\emph{labels}, ranged over by $n, n', \ldots$; 
and \emph{variables}, ranged over by $x, y, \ldots$.
\emph{Values}, ranged over $v, v', \ldots$, may include 
booleans (written $\mathtt{false}$ and $\mathtt{true}$),
integers,  names, and channels. 
We use $r$ to range over \emph{adaptation messages}: two instances are 
$\mathtt{upd}_I$ and $\mathtt{upd}_E$, for internal and external requests.
We use $\,\til{\cdot}\,$ to denote finite sequences. 
Thus, e.g., $\til{x}$ is a sequence of variables $x_1, \ldots, x_n$.
We use $\epsilon$ to denote the empty sequence.

Table~\ref{tab:syntax} reports the syntax of expressions and processes. 
Processes include usual constructs for %intra-session 
input, output, and labeled choice. 
%Communicated (\emph{delegation}).
Common forms of recursion, parallel composition, conditionals, and %name\-/\-chan\-nel 
restriction are also included.
Constructs for session establishment %(request and accept)
are annotated with a session type $\ST$,
% and on \emph{duality}, denoted $\cdual$; see~\cite{DBLP:journals/acta/GayH05} and~\S\,\ref{s:types}.
which is useful in derived static analyses.
A prefix for closing a session, inherited from~\cite{GiustoP14short}, is convenient to better structure specifications. %Also, the process syntax includes 
%Binding is as follows: 
%the channel 
Variable $x$ is bound in processes 
$\nopenr{u}{x{:}\ST}.P$, $\nopena{u}{x{:}\ST}.P$, and 
%$x$ is bound in 
$\inC{k}{x}.P$. 
Binding for name and channel restriction is as usual.
Also, recursion variable $\rv{X}$ is bound in  process $\mu \rv{X}.P$.
%Based on these intuitions, g
Given a process $P$, its sets of free/bound channels, names, variables, and recursion variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fn}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bn}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are   as expected. 
%In all cases, w
We always rely on usual notions of $\alpha$-conversion %(noted $\equiv_\alpha$) 
and (capture-avoiding) substitution, denoted 
$\subst{k}{x}$ (for channels) and $\subst{P}{\rv{X}}$ (for processes). 
We write $\subst{k_1, \ldots, k_n}{x_1, \ldots, x_n}$ to stand for an $n$-ary simultaneous substitution. 
Processes without free variables or free channels are called \emph{programs}.


Up to here, the language is essentially a  synchronous $\pi$-calculus with sessions~\cite{DBLP:conf/esop/HondaVK98}. 
As %hinted at above, 
motivated in the Introduction,
building upon 
\emph{locations} $\locf{loc}, \locf{l_1}, \locf{l_2}, \ldots$, 
%\emph{adaptation messages} (ranged over $r, r', \ldots$), 
we consider the following 
constructs 
for handling runtime adaptation:
% the following: 
\begin{enumerate}[-]
\item 
\emph{located processes}, denoted $\scomponent{\locf{loc}}{P}$; 
\item 
\emph{update processes}, denoted $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{\STT_{1}^{i}; \cdots ;\STT_{m}^{i}}{Q_i}{i \in I}}$; 
\item 
\emph{(session) monitors}, denoted $ \que{k}{\ST} $; 
\item 
\emph{location queues}, denoted $ \que{\locf{loc}}{\til{r}} $; 
and
\item 
\emph{adaptation  signals}, denoted $\outC{\locf{loc}}{r}$.
\end{enumerate}
Moreover, expressions include the 
\emph{arrival predicate}  $\arrive{\locf{loc}, r}$.


%while located processes have been central in our previous works~\cite{DBLP:conf/sac/GiustoP13,BGPZLMCS}, constructs (b)--(d) above have been first introduced in~\cite{Kouzapas12}. As 
%we explain in detail next, here we adapt these constructs to the case of runtime adaptation (an issue not explored in~\cite{Kouzapas12}).
We now comment on these elements.
%As in~\cite{DBLP:conf/sac/GiustoP13,BGPZLMCS}, given a process $P$ and a location $\locf{loc}$, 
%process $\scomponent{\locf{loc}}{P}$ denotes a \emph{located process}.
%Locations are transparent: inside \locf{loc}, process $P$ can freely evolve, possibly interacting with its environment. 
%They can be nested, which is particularly convenient when structuring processes for adaptability purposes.
\emph{Located processes} and 
\emph{update processes}
have been already discussed.
Here we just remark that 
update processes
are assumed to refer to at least one variable $x_i$ and to offer at least one alternative~$Q_i$.
Also, variables $x_1, \ldots, x_m$ are bound in 
 $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{\STT_{1}^{i}; \cdots ; \STT_{m}^{i}}{Q_i}{i \in I}}$; this process
is often abbreviated as 
 $\nadaptbig{\locf{loc}}{\mycase{\til{x}}{\STT_{1}^{i}; \cdots ; \STT_{m}^{i}}{Q_i}{i \in I}}$.
% variables $x_i$ are bound in $\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}$.
Update processes 
generalize the $\mathtt{typecase}$ introduced in~\cite{Kouzapas12}, which defines a case-like choice based on a single channel;
 in contrast,  
 to specify adaptation for locations with multiple open sessions, 
 our update processes define type-directed checks over one or more channels.
%Note that we use dynamic session type inspection only for runtime adaptation purposes, while 
%in~\cite{Kouzapas12} 
%$\mathtt{typecase}$ is part of the syntax of processes. 
%This choice enables us 
%%to focus on  the key aspects of event-based concurrency that are key to runtime adaptation. Also, it allows us 
%%the limited use of our generalized form of $\mathtt{typecase}$ is also useful 
%to retain a standard session type syntax; see~\S\,\ref{s:types}. %simplify some parts of our technical development.

Update processes go hand-in-hand with \emph{monitors}, 
runtime entities which keep the current protocol state  at a given channel. 
We write $\que{\cha^p}{\ST}$ to denote the monitor which stores the protocol state $\ST$ for 
channel $\cha^p$. 
In~\cite{Kouzapas12}, a similar construct is used to store in-transit messages in  asynchronous communication. 
For simplicity, 
%and to highlight the adaptation mechanisms of our language, 
here we consider synchronous communication; monitors store only the current protocol state. This choice is aligned with our goal of identifying the elements from the eventful session framework that are central in  runtime adaptation (cf. Remark~\ref{rem:asynch}).
%\looseness=-1
%DA TOGLIERE: Extensions of our framework to the asynchronous case are discussed in Remark X.

\emph{Location queues}, not present in~\cite{Kouzapas12}, 
%are associated to locations; they 
handle adaptation requests, modeled as a possibly empty sequence of messages $\til{r}$.
%they are denoted $\que{\locf{loc}}{\til{r}}$.
Location queues 
%They
enable us to give a unified treatment to adaptation requests, internal and external. 
%The empty queue is denoted $\que{\locf{loc}}{\epsilon}$.
Given $\que{\locf{loc}}{\til{r}}$, it is worth observing that messages $\til{r}$ are not related to communication as abstracted by session types. This represents the fact that we handle adaptation requests and structured session exchanges as orthogonal issues. 
An \emph{adaptation signal} $\outC{\locf{loc}}{r}$ enqueues request $r$ into the location queue of $\locf{loc}$.
To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues.
%
To connect  runtime adaptation and communication, our language allows the coupling of update processes with the \emph{arrival predicate on locations}, denoted \arrive{\locf{loc}, r}. %, which we now explain.
Inspired by the $\mathtt{arrive}$ predicate in~\cite{Kouzapas12}, this predicate detects if a  message $r$ 
%(which may represent a request for adaptation or upgrade) 
has been placed in the queue of  \locf{loc}. 

%Summing up, o
Our  language embodies several concerns related to runtime adaptation: using adaptation signals and location queues 
we may specify
%\emph{who} may specify/trigger an adaptation event; by using queues  it also decrees 
\emph{how} an adaptation request is issued; arrival predicates enable us to specify \emph{when} adaptation will be handled; using update processes and monitors we may specify \emph{what} is the goal of an adaptation event. 



%, noted $\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).


\begin{table}%[h!]
\[
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \pired \restr{\cha}{\big({\locc{P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} }\big) } \quad (\ST \cdual \STT) \vspace{2mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\STT}}} 
\pired \locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } 
%\quad (\ST \cdual \STT) %\quad ({e} \downarrow {c}) 
\vspace{2mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J}\! \para\!  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}}\! \para \!
\locd{\select{\cha^{\,\overline{p}}}{n_i};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}} } 
 \pired   C\{P_i \para \que{\cha^p}{\ST_i} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\STT_i} \}  
\quad (%\ST_i \cdual \STT_i,\, 
i \in J)  
\vspace{2mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\tend} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\tend}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{2mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
%\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
%\vspace{2mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{2mm}
% \\ 
\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
\vspace{2mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{2mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{2mm}\\
\rulename{r:IfTrue} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{2mm}
\\
 \rulename{r:IfFalse} &
\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{2mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{2.5mm}\\
\rulename{r:Arr1} & 
\displaystyle\frac{ \til{r} =  r_1 \cdot \til{r_0} }{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{true}]}
\para \locd{\que{\locf{loc}}{\til{r_0}}} }  
\vspace{2.5mm}\\
\rulename{r:Arr2} & \displaystyle\frac{ (\til{r} = r_2 \cdot \til{r_0}  \land r_1 \neq r_2) \lor \til{r} = \epsilon}{
\locc{\evc{E}[\arrive{\locf{loc},r_1}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{false}]}
\para \locd{\que{\locf{loc}}{\til{r}}} }  
\vspace{2.5mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:UpdOld} & 
%\displaystyle\frac{
%\begin{array}{rcl} 
%\multicolumn{3}{c}{\mathsf{fc}(P)  = \cha_1^p, \ldots, \cha^p_n }
%%& &
%%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
%\\
% (V = P \land R' = R) & \bigvee  & \big(
% \mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) ~ \land~
%\\ 
%&& ~~~ V = Q_l\subst{\til{\cha}\,}{\,\til{x}_0} ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para\! \cdots\! \para \que{\cha^p_n}{\STT^{l}_n} 
%  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P \para R}} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
%\end{array}
%} 
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad \forall j \in [1,..,m]. (\Pin{P}{\que{\cha^p_j}{\ST_j}})}
%& &
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
\\
 (V = P) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
 V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m} 
  \big)
\end{array}
}{
%\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{\STT_{1}^{i}; \cdots ; \STT_{m}^{i}}{Q_i}{i \in I}}}   
\pired   %\\
 \locc{\scomponent{\locf{loc}}{V}} \para \locd{\mathbf{0}}
%\end{array}
} 
\end{array}
%\vspace{-3mm}
\]
\caption{Reduction Semantics for Binary Processes.
Above, $\ST$ and $\STT$ denote session types. % (cf. Def.~\ref{d:types})
\label{tab:redsem-full}}
%\vspace{-7mm}
\end{table}

\paragraph{\textbf{Semantics.}}
The semantics of our language is given by a \emph{reduction semantics},
the smallest relation generated by the rules 
in Table~\ref{tab:redsem-full}.
We write $P \pired P'$ for the reduction from $P$ to $P'$.
Reduction relies on 
%an evaluation relation on expressions, denoted $e \downarrow v$ (where $v$ is a value). Also, it uses 
a standard notion of structural congruence, denoted~$\equiv$ (see~Appendix \ref{app:types}). %. (TO BE ADDED)
It also relies on  \emph{evaluation} and \emph{location} contexts:
\begin{eqnarray*}
\evc{E}  ::=  - \sepr \outC{k}{\evc{-}}.P \sepr  \ifte{\evc{-}}{P}{Q} \qquad \quad
C,D  ::=  - \sepr \scomponent{\locf{loc}}{C \para P}
\end{eqnarray*}
Given 
$\locc{\!\!-\!\!}$
 (resp. $\evc{E}[-]$), we write $\locc{P}$ (resp. $\evc{E}[e]$) to denote 
the process (resp. expression) obtained by filling in occurrences of hole $-$
in $C$ with $P$ (resp. in $\evc{E}$ with~$e$). 
%The extension of $\equiv$ to contexts is as expected.

We comment on the reduction rules below. 
The first four rules formalize session behavior within hierarchies of nested locations.
Using duality for session types, denoted $\cdual$ (cf. Definition~\ref{d:subt}),
in rule~\rulename{r:Open} the synchronization on a name $u$ %with dual session types 
leads to establish a session on fresh channels $\cha^p$ and $\cha^{\overline{p}}$;
also, two  monitors with the declared session types are created.
Duality for polarities $p$ is as expected: $\overline{+} = -$ and  $\overline{-} = +$.
By construction, 
monitors are \emph{local}, i.e., they are created in the same contexts in which the session is established. 
Rule~\rulename{r:Com} represents  communication of a value: we require both complementary prefixes and that the monitors support input and output actions. After reduction, prefixes in processes and monitors are consumed.  
Similarly, rule~\rulename{r:Sel} for labeled choice is standard, augmented with monitors. %, which should support branching and selection. 
Rule~\rulename{r:Clo} formalizes  session termination, discarding involved monitors.
The monitors in these three rules allow us to track the evolution of active session protocols. 
%It is worth observing that we require that session queues are \emph{local} to the process. This way, for instance, a process 
%\begin{equation}
%\locc{\outCn{\overline{\cha}^{\,p}}{v}.P} \para \loccp{\que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}} \nonumber
%\end{equation}
%is not able to reduce for the queue $ \cha^p$ is not local to the process executing that session.



The remaining rules in Table~\ref{tab:redsem-full} 
define our event-based approach to runtime adaptation. 
They require the following auxiliary definition:
\begin{mydef}[Matching]\label{d:matchp}
Given an index set $I$, 
session types $\ST_1, \ldots, \ST_m$, 
an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
and an  $l \in I$,
we write 
\begin{equation*}
\mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) 
\end{equation*}
if and only if $\forall n < l.(\exists j \in [1..m].~\STT^{n}_j \not\csub \ST_j)
\land (\bigwedge_{h \in [1..m]} \STT^{l}_h \csub \ST_h)$.
\end{mydef}

We may now return to describing the reduction rules:
\begin{enumerate}[$-$]
\item Rule~\rulename{r:UReq} treats the issue of an adaptation request $r$ as a synchronization between a location queue and an adaptation signal. The queue and the signal may be in different  contexts;  this enables ``remote'' requests. 
\item Rules~\rulename{r:Arr1} and \rulename{r:Arr2} resolve arrival predicates %within evaluation contexts
by querying the (possibly remote) queue $\til{r}$. 
\item Rule~\rulename{r:Upd} defines the update of the current protocol at location \locf{loc}, which is given 
by an indexed set of open sessions with their associated monitors.
%While at a first sight it may appear complex, the rule actually enforces a simple case operation over the running sessions at location \locf{loc}. The rule attempts to match (via subtyping, noted  $\csub$ in~\S\,\ref{s:types}) the current protocol state at \locf{loc} (embodied by the open sessions $\til{\cha}$ and their associated queues $R$) with the different options offered by the update process. The rule focuses on finding the first positive match; if no such 
%match exists then the current behavior at \locf{loc} ($P$, in the rule) is left unchanged, and the update process is consumed.\looseness=-1 
The rule attempts to match such a set with the first suitable option offered by an update process for \locf{loc}.
If there is no matching alternative the current protocol state at \locf{loc} is kept unchanged. %, and the update process is consumed.
By an abuse of notation, we write
$\Pin{P}{P_1}$ 
to indicate that $P_1$ occurs in $P$, i.e., 
if $P = C[P_1]$ for some  $C$.
Formally, 
given an index set $I$ over the update process, 
suitability with respect to the behavior at \locf{loc}
is defined 
by predicate $\mathsf{match}_I$ (cf. Definition~\ref{d:matchp}). 
Using subtyping $\csub$ (cf. Definition~\ref{d:subt}), the predicate holds for an $l \in I$ which 
defines a new protocol state.
\end{enumerate}

%\begin{definition}[Matching (Old)]\label{d:matchp}
%Given an index set $I$, session channels $\til{\cha}$, sets of variables $\til{x}$ and $\til{x}_0$,
%an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
%an indexed set of processes $\{Q_i\}_{i \in I}$, 
%and an  $l \in I$,
%we write 
%\begin{equation}
%\mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) \nonumber
%\end{equation}
%if and only if all of the following hold:
%\begin{enumerate}[(a)]
%\item $\til{x}_0 \subseteq \til{x} \land %\til{x}_0 = \{x_1, \ldots, x_g\} \land \til{\cha} = \{\cha^p_1, \ldots, \cha^p_n\} \land 
%|\til{x}_0| = |\til{\cha}| = n \land n \leq m$
%\item $\exists I' \subseteq I.(\forall h \in I'. \mathsf{fc}(Q_h) = \til{x}_0 \land l \in I')$
%\item $\forall r < l.\exists j \in [1..n].\exists s \in [1..n].~~\STT^{r}_s \not\csub \ST_j
%~~\land~~\forall j \in [1..n].\forall s \in [1..n].~~ \STT^{l}_s \csub \ST_j $
%\end{enumerate}
%\end{definition}
%Hence,  $\til{x}_0$ denotes a set of variables of the same cardinality of $\til{\cha}$ (condition (a)).
%Using $\til{x}_0$, condition (b) singles out the subset $I'$ of $I$ of suitable candidates for adaptation routines; index $l$ must be in $I'$. Condition (c) formalizes the fact that index $l$ refers to the first alternative to match, up to subtyping. 





In addition, our  semantics includes 
standard and/or self-explanatory treatments for
reduction under evaluation contexts, parallel composition, located context, and restriction.
Also, it accounts for applications of structural congruence, recursion and conditionals.
%(with omitted rule~\rulename{r:IfFalse} being as expected).\looseness=-1 


%Hence,  the matching predicate formalizes the fact that index $l$ refers to the first alternative that matches,  up to subtyping. 

%\noindent{\bf Example.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\input{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{myexamp}
Recall process $W$ given in the Introduction. 
%\begin{equation}
%W  =   \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST}.P^{50}} \para  \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT}.Q}\,} \nonumber
%\end{equation}
According to our semantics: % we have:
\begin{eqnarray*}
W & \pired& \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P\subst{\cha^p}{x} \para \que{\cha^p}{\ST_{\mathtt{buy}}}} \para  \scomponentbig{\locf{seller}}{Q\subst{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT_{\mathtt{sel}}}}\,} \big)}  \\ 
& \pired^2 & \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P' \para \que{\cha^p}{\ST_{\mathtt{pay}}}} \para  \scomponentbig{\locf{seller}}{Q' \para \que{\cha^{\overline{p}}}{\STT_{\mathtt{pay}}}}\,} \big)} 
\end{eqnarray*}
Suppose that following an external request the seller must offer a new payment method. (a gift card).
Precisely, we would like \pt{S} to act according to the   type
$\STT_{\mathtt{gift}}$ given in the Introduction.
%\begin{equation*}
%\STT_{\mathtt{gift}} \,=\,\&\{\mathtt{addItem}:\, \&\{\mathtt{giftc}:\, \STT_\mathtt{gc} \,,\, \mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} 
%\end{equation*}
Let $\ST_{\mathtt{gift}}$ be the dual of $\STT_{\mathtt{gift}}$.
We then may define the following update process $R^1_{xy}$:
\begin{equation*}
{\nadaptbig{\locf{sys}}{\mycase{{x,y}}{\ST^{}_{\mathtt{pay}} \,;\, \STT^{}_{\mathtt{pay}}}{\scomponentbig{\locf{buyer}}{ P' \para \que{x}{\ST_{\mathtt{gift}}}} \para  \scomponentbig{\locf{seller}}{Q'' \para \que{y}{\STT_{\mathtt{gift}}}}}{}}} 
\end{equation*}
Thus, $R^1_{xy}$ keeps the expected implementation for the buyer ($P'$), but updates its associated monitor.
For the seller, both the implementation and monitor are updated; above, $Q''$ stands for a process offering the three payment methods.
We may then specify the whole system as:
%\begin{equation}
$W \para \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{R^1_{xy}}{\rv{X}}$.  
The type system introduced next  ensures, among other things, that updates such as $R^1_{xy}$ consider both a process and its associated monitors, ruling out the possibility of discarding the monitors that enable reduction. 
\end{myexamp}


\section{Session Types for Eventful Runtime Adaptation}\label{s:types}
This section introduces a session type system for the process language of \S\,\ref{s:evadap}.
Our main result (Theorem~\ref{t:safety}) is that well-typed programs enjoy both \emph{safety} (absence of runtime communication errors)
and \emph{consistency} properties (update actions do not disrupt established sessions).
Our development follows the lines of the typed framework in~\cite{GiustoP14short}. 
%\begin{definition}[Types]\label{d:types}
%The syntax of \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) 
%and \emph{session types} (ranged over by $\ST, \STT, \ldots$)
%is given below. We use $T, S, \ldots$ to range over $\capab, \ST$.
%\[
%\begin{array}{lclr}
%%T, S&::=& \capab, \ST \\
%\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\
%
%\ST, \STT &::=  &  !(\capab).\ST \sepr ?(\capab).\ST  \sepr !(\STT).\ST \sepr ?(\STT).\ST  \quad& \text{send, receive, throw, catch} \vspace{0.5mm}\\ 
%		& \sepr &  \&\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \} \sepr \oplus\{n_1{:}\ST_1 \dots  n_m{:}\ST_m \}  &  \text{branch, select} \vspace{0.5mm} \\
%		& \sepr &  \tend \!\!\!\!\!\!& \text{closed session} \vspace{0.5mm} \\
%    & \sepr  & t \sepr  \mu t.\ST & \text{type variable, recursion} 
%\end{array}
%\] %}
%\end{definition}
%\noindent 

The syntax of session types (ranged over by $\ST, \STT, \ldots$) has been already presented in \S\ref{s:overv}.
We consider \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) and
write $T, S, \ldots$ to range over $\capab, \ST$.
Therefore, although our process language copes with runtime adaptation, 
our type syntax is standard and retains the intuitive meaning of session types~\cite{DBLP:conf/esop/HondaVK98}, which we now briefly recall.
Type $?({\capab}).\ST$ (resp. $?(\STT).\ST$) abstracts the behavior of a channel 
which receives %a boolean or a name 
a value of type $\capab$
(resp. a channel of type $\STT$) 
and then continues as $\ST$. 
Dually, type $!({\capab}).\ST$ (resp. $!(\STT).\ST$) represents the behavior
of a channel which sends 
a value of type $\capab$
%a value (resp. a channel) 
 and then continues as $\ST$.
Type $\&\{n_1:\ST_1 \dots  n_m:\ST_m \}$ describes a branching behavior:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\ST_1 \dots  n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\ST_1, \ldots, \ST_m$ and then continues as $\ST_j$.
We use $\tend$ to type a channel with no communication behavior. Type $\mu t.\ST$ describes recursive behavior;  
as usual, we consider recursive types under equi-recursive and contractive assumptions.

Along the paper we have informally appealed to \emph{duality}  and \emph{subtyping}  over session types (denoted \cdual and \csub, resp.). 
Since our session type structure is completely standard, 
we may rely on the (coinductive) definitions given by Gay and Hole~\cite{DBLP:journals/acta/GayH05}, which are standard and well-understood --- see also Definition~\ref{d:subt}.

%The extension of $\csub$ to typings $\ActS$ % ,  written $\ActS \csub \ActS'$, 
%is as expected.

%The former relies on a \emph{duality relation}; % (cf. Def.~\ref{def:dualr} in~\cite{GiustoP14ext};
%the latter uses the  notion of \emph{type simulation}. % (given by Def.~\ref{def:simul} in).
%For the sake of space, we refer to~\cite{GiustoP14ext} for full definitions of these two notions.
%
%\begin{definition}\label{d:subt} Let $T, S$ be types.
%%\begin{enumerate}[$-$]
%%\item 
%The \emph{coinductive duality relation}, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
%such that $(T, S) \in \mcc{R}$. 
%%\item 
%The \emph{coinductive subtyping relation}, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{S}$
%such that $(T, S) \in \mcc{S}$. \\
%The extension of $\csub$ to typings,  written $\ActS \csub \ActS'$, 
%arises as expected.
%%\end{enumerate}
%\end{definition}




Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$.
Based on the syntactic occurrences of session establishment prefixes $\nopenr{a}{x{:}\ST}$, and $\nopena{a}{x{:}\ST}$,
the interface of a process describes the %(possibly persistent) 
services appearing in it.
We 
annotate services with a 
\emph{qualification} $\qua$, which may be `$\qual$' (linear) or `$\quau$' (unrestricted).
Thus, %intuitively, 
the interface of a process gives an ``upper bound'' on the services that it  may execute.
The typing system uses interfaces to control the behavior contained by locations after an update.
We have:


\begin{mydef}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements  is
$\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$ (i.e., a set of  
assignments from names to qualified session types).
%More precisely: $\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$, 
%\text{$u$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We write $dom(\INT)$ to denote the set $\{u \mid u:\ST_\qua \in \INT \}$ and  $\#_\INT(a) = h$ to mean that  $a$ occurs $h$ times in $\INT$. 
\end{mydef}
%Thus, several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces %$\INT_1$ and $\INT_2$ 
is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.
Moreover, we write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
We now define an ordering relation over interfaces, relying on subtyping:

%Next definition, extends the  subtyping relation to interfaces..

\begin{mydef}[Interface Ordering] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exist $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{mydef}


%\subsection{Environments, Judgments and Typing Rules}
% \begin{table}[t]
% \textsc{Environments}
% $$
% \begin{array}{lclr}
% 		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
% \ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
% \Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment} \vspace{0.5mm} \\
% \Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
% \end{array}
% $$  
% \caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
% \end{table}
% 

\begin{table}%[t]
\[
\begin{array}{c}

\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\quad \infer[\rulename{t:Que}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{k}{\ST}}{\type{k:\que{}{\ST}}{\emptyset}}}{}
%\vspace{2mm} \\
\quad
\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} 
\quad
\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}
\vspace{2mm} \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} 
\quad 
\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}}
\vspace{2mm} \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
 \qquad
 \infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Acc}]
{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \ST \quad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
%\vspace{2mm} \\
\quad
\inferrule*[right=\rulename{t:Req}]
 {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \STT \quad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
\vspace{2mm} \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
\vspace{2mm} \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{\STT_{1}^{j}; \cdots ;\STT_{m}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{
%\begin{array}{c}
\typing{\Theta}{\locf{loc}}{\INT} \qquad \forall j \in J, \ \mathsf{fv}(Q_j) \setminus \{x_1, \ldots, x_m\} = \emptyset \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q_j}{\type{x_{1}{:}\mon{\STT_{1}^{j}}; \cdots ;x_{m}{:}\mon{\STT_{m}^{j}}}{\INT_j} }  \qquad \INT_j \intpr \INT
%\end{array}
}
% \text{ where } \typeque{x:\STT} \text{ stands for } x:\STT, x:\que{}{\STT}
\vspace{2mm} \\
%\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
%\qquad
%\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
%{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
%\vspace{2mm} \\
  \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^p:\mon{\ST_1}, \cha^{\overline{p}}:\mon{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} 
\quad 
 \infer[\!\!\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
\vspace{2mm} \\
\infer[\!\!\rulename{t:sub} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \intpr \INT'}
% \vspace{2mm} \\
% \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
% {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
 %\text{ where } \INT_u \text{ contains only declarations for } u \ (i.e. \forall v\neq u, v\notin \dom{\INT_u} )
 \end{array}
 \]
\caption{Well-Typed Processes: Typing Rules (Part I).} \label{tab:ts}
%\vspace{-8mm}
\end{table}




\noindent 
We now define our typing environments. % on which our type system relies.
We write $\qua$ to range over 
qualifiers
$\qual$ and $\quau$. 
\[
\begin{array}{lclr}
%		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, u:\langle \ST_\qua , \STT_\qua \rangle \quad& \text{first-order environment (with $\ST_\qua \cdual \STT_\qua$)} \vspace{0.5mm} \\
\Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,\locf{loc}:\INT     \quad& \text{higher-order environment}
\end{array}
\]  
We consider typings $\ActS$ and environments $\Gamma$ and $\Theta$. 
Typing $\ActS$  collects
assignments from channels to session types; it describes
currently active sessions. 
In our system, 
$\ActS$ also includes \emph{bracketed assignments}, denoted $\kappa^p:\que{}{\ST}$,
which represent the type for monitors. 
Subtyping extends to these assignments ($\que{}{\ST} \csub \que{}{\STT}$ if  $\ST \csub \STT$) 
and thus to typings.
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor k^p:\que{}{\ST} \in \ActS\}$. 
We write $\ActS , k:\ST $  where $k \not\in dom(\ActS)$.
Furthermore, we 
write $\ActS, k:\mon{\ST}$ to 
abbreviate $\ActS, k:\ST, k:\que{}{\ST}$.
That is, $k:\mon{\ST}$  describes both a session and its associated monitor.
%The extension of $\csub$ to typings $\ActS$ is as expected.


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of qualified session types.
As motivated earlier, a session type is qualified with 
`$\quau$' if it is associated to a unrestricted/persistent service; otherwise, it is qualified with 
`$\qual$'. 
The higher-order environment $\Theta$ 
collects assignments of typings to process variables and interfaces to locations.
While the former concerns recursive processes, the latter concerns located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form \looseness=-1
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$$
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.
Typing rules are shown in Tables~\ref{tab:ts} and~\ref{t:addtyperules}.
%(remaining rules can be found in~\cite{GiustoP14ext}).
%remaining rules can be found in Table~\ref{t:addtyperules} (Appendix~\ref{ap:adtyping}).
Below we comment on some  of the rules in Table~\ref{tab:ts}: the rest are standard and/or self explanatory.
Rule \rulename{t:Adapt} types update processes. Notice that the typing rule  ensures that each process $Q_i$ has exactly the same active sessions that those declared in the respective case.   
Also, we require that alternatives contain both processes and monitors. 
With
$\INT_j \intpr \INT$ we guarantee that the process behavior does not ``exceed'' the expected behavior within the location.
Rule~\rulename{t:sub} takes care of  subtyping both for typings $\ActS$ and interfaces. Rule~\rulename{t:CRes} types channel restriction that ensures typing duality among partners of a session and their respective queues.
Typing of queues is given by rule \rulename{t:Que} that simply assigns  type $k:\que{}{\ST}$ to queue $\que{k}{\ST}$.
Finally, rule \rulename{t:NRes} types hiding of service names, by simply removing their declarations from the interface $\INT$ of the process.
In the rule, 
$\INT_u$ contains only declarations for $u$, i.e., $\forall v\neq u, v\notin \dom{\INT_u}$.

\begin{table}%[!t]
{\small
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{u}{\name}}{} 
%\vspace{1.5mm} \\
\quad
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\vspace{2mm} \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{d=u \vee d=\kappa^p \vee d =x} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, u:\langle\ST_\qua, {\STT}_\qua\rangle}{u}{\langle\ST_\qua, {\STT}_\qua\rangle}}{\ST \cdual \STT } 
%\vspace{2mm} \\
\qquad
\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{2mm} \\
%\inferrule*[right=\rulename{t:Accept}]
%{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \alpha \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
%\vspace{2mm} \\
%\inferrule*[right=\rulename{t:Request}]
% {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \STT \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
%\vspace{2mm} \\
%\inferrule*[right=\rulename{t:Clo}]
% {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
%\quad
%\inferrule*[right=\rulename{t:Par}]
% {
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
%
%\vspace{2mm} \\
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\qquad
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\quad 
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
 
\quad
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad u \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT }}}


\vspace{2mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$
}
\caption{Well-Typed Processes: Typing Rules (Part II).\label{t:addtyperules}}
\end{table}


Our type system enjoys the standard \emph{subject reduction} property. 
We rely on \emph{balanced} typings: $\ActS$ is balanced iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $\kappa^p:\que{}{\ST} \in \ActS$)
then also 
$\kappa^{\overline{p}}: \STT \in \ActS$ (resp. $\kappa^{\overline{p}}: \que{}{\STT} \in \ActS$), with $\ST \cdual \STT$.


\begin{mytheo}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{mytheo}

\begin{proof}
By induction on the last rule applied in the reduction. %; it adapts the one given in \cite{GiustoP14short}
See Appendix~\ref{app:proofs} for details.
\end{proof}

We now define and state \emph{safety} and \emph{consistency} properties. 
While safety  guarantees  adherence to prescribed session types and absence of runtime errors, consistency 
%is unique to our framework with runtime adaptation and
ensures that sessions are not jeopardized by 
careless
%incautious 
 runtime adaptation actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.

\begin{mydef}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa^p$, i.e., 
$P$ is one of the following:
\[
\inC{\kappa^{\,p}}{x}.P'  \qquad \outCn{\overline{\kappa}^{\,p}}{v}.P' \qquad      \close{\kappa^{\,p}}.P' \qquad \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  \qquad   \select{\kappa^{\,p}}{n}.P'
%\begin{array}{lclcl}
%    \inC{\kappa^{\,p}}{x}.P' & \qquad &  \outCn{\overline{\kappa}^{\,p}}{v}.P' & \qquad &     \close{\kappa^{\,p}}.P'    \\
%   \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  &  \quad&   \select{\kappa^{\,p}}{n}.P'  & \quad& 
%\end{array}
\]
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities.
$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{mydef}


Informally, a process $P$
is called \emph{consistent} 
if whenever  it has a $\kappa$-redex  then  update actions do not destroy such a redex.  Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$. We then define:

\begin{mydef}[Safety and Consistency]\label{d:consis}
Let $P$ be a process.
\begin{enumerate}[$-$]
\item We say $P$ is \emph{safe} if it never reduces into an error. 
\item We say $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{enumerate}
\end{mydef}


We now state our main result; it follows as a  consequence of Theorem~\ref{th:subred}.
 
\begin{mytheo}[Typing Ensures Safety and Consistency]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then program $P$ is update consistent and %never reduces into an error.
safe.
\end{mytheo}

\begin{myremark}[Asynchronous Communication]\label{rem:asynch}
We have focused on \emph{synchronous} communication: this allows us to give a compact semantics, relying on a standard type structure.
% in which our novel adaptation mechanisms can be cleanly presented. 
To account for asynchrony, we would require 
a runtime syntax for programs with 
queues for in-transit messages (values, sessions, labels). %; such queues would become part of the runtime syntax of programs. 
The type system must be extended to accommodate these new runtime processes. 
In our case, an extension with asynchrony  
would rely on the machinery defined in~\cite{Kouzapas12} and it is presented in next section for multiparty communications.
\end{myremark}

\begin{myremark}[Incremental Adaptation]
Adaptation in our framework is ``incremental'' in that changes always preserve/extend active session protocols, exploiting subtyping for enhanced flexibility.
Our framework can be modified so that arbitrary protocols are installed
as a result of an update. One would need to 
 ensure that the two endpoints of a session are present in the same location: 
 arbitrary  updates are safe as long as both endpoints %(two, in our binary case)
 are simultaneously updated with dual protocols.
% modify the operational semantics and the typing rules to
This alternative requires modifying definitions for session matching (Definition~\ref{d:matchp}) and interface ordering (Definition~\ref{d:rintpre}).
\end{myremark}

%\input{types.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%Another difference is that in~\cite{DBLP:conf/aplas/AndersonR12} update actions are independent from the program's syntax.

%\section{Concluding Remarks}\label{s:concl}


\section{Event-Based Adaptation for Multiparty Communications}\label{s:multi}
Here we present a generalization of our approach to 
adaptation to the case of 
multiparty communications. 
As we explain in the Introduction, 
we present a proof of concept that illustrates 
how type-directed constructs for adaptation and eventful constructs for handling adaptation requests
can be integrated into an existing framework for self-adaptable multiparty sessions, namely the 
framework put forward by Coppo et al. in~\cite{CDV15j} (and 
summarized in \S\,\ref{ss:multisumm}).
%whose main features are summarized in \S\,\ref{ss:dezani}.
%Then, in \S\,\ref{ss:eventdezani} we present our generalization, showing how
%event-based adaptation and multiparty session communication can be jointly treated.

%We believe that adaptation and session communication are orthogonal matters and in order to ease the understanding of foundational principles, we explain how our approach can be integrated into an existing proposal for adaptable multiparty sessions~\cite{CDV15j}.

%%\subsection{Adding Events}\label{ss:eventdezani}
In essence, 
%We now modify the approach overviewed in \S\,\ref{s:overv} to account with event-based adaptation. 
we modify the adaptation approach of~\cite{CDV15j} with event-based constructs; the main advantage of this approach is a separation between communication actions from adaptation mechanisms.
In the framework of~\cite{CDV15j} these two issues are tied together, as adaptation flags occur within global type specifications at the same level of protocol exchanges. An event-based approach enables us to treat adaptation 
at the level of processes. In our opinion, the resulting separation of communication and adaptation concerns 
is beneficial for specification and analysis. 

%\red{qui spiegherei le ragioni della scelta: e.g. adaptation intesa come evento straordinario e non previsto a priori}
At the technical level, the addition of events entails novelties at the level of global types and networks:
%the explicit adaptation synchronization specified by global protocols is eliminated; also, 
as 
monitored processes will be now embedded into distributed locations which contain 
local collections and 
queues that govern local and external adaptation. 
Furthermore, at the level of processes we replace processes 
$c?l(\lambda, \mathtt{T}).P$, and $c!l(\lambda(F),\mathtt{T} ).P$
with a single construct $c!(\gtype{G}).P$ which 
enforces a locally-motivated adaptation based on global type $\gtype{G}$.
In some sense, $c!(\gtype{G}).P$ corresponds to the flag-issued adaptation of~\cite{CDV15j}, which is specified  the system itself: a protocol participant signals to the others that they all should adapt to
execute protocol $\gtype{G}$.
Overall, we have a   two-level framework of processes and systems, instead of  processes, networks, and systems.



\subsection{Syntax}
\paragraph{Global Types.}
We use \emph{global types} to specify the structured interaction between two or more participants.
 We wish to distinguish between communication and adaptation concerns; for this reason, unlike~\cite{CDV15j}, our global types do not mention synchronizations related to adaptation. 
We write  $\pt{p}, \pt{q}, \pt{r}, \ldots$  and $\Pi, \Pi', \ldots$ 
to denote participants
and sets of participants, respectively.
Exchange of values take place on labels, here denoted $\lambda, \lambda', \ldots$, which are useful to express choices. 
We write $\locf{loc}, \locf{loc}', \ldots$ to range over locations.
As in~\cite{CDV15j}, we assume that communicated values are extracted from a set of sorts $S$. 
Formally, we have:
\begin{mydef}[Global Types] The set of \emph{global types} is defined by
\[
\gtype{G} ::= \pt{p} \to \pt{q} :\{\lambda_i(S_i).\gtype{G}_i\}_{i\in I} \sepr \mathsf{end}
\] 
\end{mydef}
As we follow~\cite{CDV15j}, our syntax of global types is admittedly simple: a global type 
$\pt{p} \to \pt{q} :\{\lambda_i(S_i).\gtype{G}_i\}_{i\in I}$
represents a labeled communication from participant $\pt{p}$ to  participant $\pt{q}$.
Global type $\mathsf{end}$ denotes the terminated protocol.
We write $\pa(\gtype{G})$ to denote the set of participants declared in~$\gtype{G}$.

\paragraph{Monitors.}
In the approach in~\cite{CDV15j}, 
monitors correspond to the local view that participants have of a global type. 
In fact, monitors are used to enable actions of the process implementations;
they also contain information on the participants and labels involved in the directed exchanges. We have:
\begin{mydef}[Monitors] The set of \emph{monitors} is 
is defined by:
\[
\moni{M} ::= \pt{p}?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} \sepr \pt{p}!\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} \sepr  \mathsf{end}
\] 
\end{mydef}

An input monitor 
$\pt{p}?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I}$
can be associated to a process which can receive, for each $i \in I$, a value of sort $S_i$ with label $\lambda_i$, with a continuation that is associated to $\moni{M}_i$ (external choice). 
The output monitor 
$\pt{p}!\{\lambda_i(S_i).\moni{M}_i\}_{i\in I}$
is completely dual: it can be associated to a process which sends a value of sort $S_i$, distinguished by label $\lambda_i$, for each $i \in I$, with a continuation that is associated to $\moni{M}_i$ (internal choice). 

Following the approach of multiparty session types~\cite{DBLP:conf/popl/HondaYC08}, the monitor of a participant is obtained via a \emph{projection function}, defined below.
\begin{mydef}[Projection of a Global Type]
Given a global type $\gtype{G}$, 
the projection of $\gtype{G}$ onto a monitor for a participant $\pt{p}$, denoted $\proje{\gtype{G}}{\pt{p}}$, is defined as follows:
\begin{enumerate}[$\bullet$]
\item $\proje{(\pt{p} \to \pt{q} :\{\lambda_i(S_i).\gtype{G}_i\}_{i\in I})}{\pt{r}} ~=~
\begin{cases} 
\pt{p}?\{\lambda_i(S_i).\proje{\gtype{G}_i}{\pt{r}}\}_{i\in I} & \text{if $\pt{r} = \pt{q}$} \\ 
\pt{q}!\{\lambda_i(S_i).\proje{\gtype{G}_i}{\pt{r}}\}_{i\in I} & \text{if $\pt{r} = \pt{p}$} \\
\proje{\gtype{G}_1}{\pt{r}} & \text{if $\pt{r} \neq \pt{p}$ and $\pt{r} \neq \pt{q}$ and $\proje{\gtype{G}_i}{\pt{r}} = \proje{\gtype{G}_j}{\pt{r}}$ for all $i,j \in I$}
\end{cases}$
\item $\proje{\mathsf{end}}{\pt{r}} ~=~ \mathsf{end}$
\end{enumerate}
\end{mydef}

We will say that a global type is \emph{well-formed} if its projections are defined for all participants.
We shall work only with well-formed global types.
We assume 
that each well-formed $\gtype{G}$ is associated with 
a mapping $\mathcal{L}_\gtype{G}$ from participants to locations such that %: % $\locf{l},\locf{l'}, \ldots$:
$\pt{p} \neq \pt{p}'$ implies $\mathcal{L}(\pt{p}) \neq  \mathcal{L}(\pt{p}')$, for all $\pt{p}, \pt{p}' \in \pa({\gtype{G}})$.


\paragraph{Processes and Networks.}
Processes abstract the protocol implementations for each participant.
The association of a process $P$ with an appropriate monitor $\moni{M}$
results into a \emph{monitored process} 
$\monpro{\moni{M}}{P}$, which 
realizes the behavior of a single participant.
As hinted at above, the main differences of our framework with respect to~\cite{CDV15j}
appear at the level of monitored processes and networks (collections of monitored processes).

The definition of processes implementing multiparty services, given next, is rather standard. 
We have operators for sending and receiving messages, conditionals,  and recursion. 
On top of these standard operators we add a primitive for broadcasting 
an \emph{internal adaptation request}, denoted $c!(\gtype{G}).P$.
Intuitively, this primitive 
is an output action which mentions a new global type to be 
implemented by protocol participants.




\begin{mydef}[Processes]\label{d:processes}
The syntax of processes 
 %A process $P$ 
 is defined as:
\begin{eqnarray*}
 P & ::= 
% & c?\lambda(x).P 
 & c?\{\lambda_i(x_i).P_i\}_{i \in I} 
 \sepr c!\lambda(e).P \sepr c!(\gtype{G}).P  
 \sepr  \mu \rv{X}.P \sepr  \rv{X} 
 %\sepr  P + P 
 \sepr \ifte{e}{P}{Q}  \sepr  \nil
\end{eqnarray*}
\end{mydef}

Each process owns a unique channel, denoted $y$. 
Given a session $\cha$ and a participant $\pt{p}$, 
channel $y$ in the user code is substituted at runtime
by a session channel $\cha[\pt{p}]$. In the following
we write $c$ to denote either $y$ (the user channel) or $\cha[\pt{p}]$ (the session channel).
We assume that processes pass around expressions, defined as expected. 
Every expression $e$ reduces to a value $v$; this is denoted $e \leadsto v$.

As a simple example of internal adaptation requests, suppose 
participants $\pt{p}_1, \ldots, \pt{p}_j, \ldots, \pt{p}_n$ establish  
session $\cha$ to communicate according to a specific application/protocol (say, $\gtype{Skype}$).
To request a change of protocol, participant $j$ may issue an adaptation request to all its partners
by including the process 
$\cha[\pt{p}_j]!(\gtype{GTalk}).P$
in its local implementation.
As we will formalize later on, this request will arrive to the event queue of 
session $\cha$, and then all participants will proceed 
to adapt their local behavior to the new global type $\gtype{GTalk}$.

Our 
notion of 
networks 
departs significantly from that in~\cite{CDV15j} by considering an explicitly distributed setting in 
based on locations. 
Each location represents a distinguished site in which a determined participant resides:
it iss
composed of  
a monitored process $\monpro{\moni{M}}{P}$, % (where $\moni{M}$ is a monitor and $P$ is a process), a 
a local collection of typed processes $\Pool$
(i.e., a set of pairs $(Q, T)$ where $Q$ is a process and $T$ is its corresponding type), 
and a queue $\que{\locf{loc}}{r}$ (where $r$ stands for an \emph{external} adaptation request):
$$
\scomponent{\locf{loc}}{\monpro{\moni{M} }{P};\Pool;\que{\locf{loc}}{r}}
$$
A  location represents a place where several programs can be executed, e.g., 
the operating system of a smartphone which encloses/contains different, distinguished applications. 
For the sake of simplicity, we assume that in each location only one session can be active; 
  a generalized setting in which a  location contains more than one session is also possible, at the price of more involved machinery. We prefer having a simple setting in which the benefits of an event-based approach can be more directly appreciated.
The queue of a location connects it to a non specified environment that can (i)~add new applications to the collection (or upgrade the implementation of an existing application), or (ii) update the behavior of a monitored process. 
This is similar to the update processes for the binary framework. 
%n active session: e.g., send a new implementation correcting some bugs but leaving unchanged (up to sub-typing) the expected behavior of the service.
%\red{sottolinerei che sessioni intralaced sono facili da generalizzare partendo da questo approccio pur complicando le regole di tipaggio}
%\paragraph{Networks.}
We now formally define networks:


\begin{mydef}[Network]\label{d:networks}
  The syntax of  \emph{networks} $N$ and \emph{adaptation requests} $r$ is defined as
 \begin{eqnarray*}
 N & ::= & \new(\gtype{G}) 
 \sepr \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool;\que{\locf{loc}}{r}}
 \sepr \scomponent{\locf{loc}}{\Pool;\que{\locf{loc}}{r}} 
 ~\sepr~ \kappa: h 
 \sepr  \que{\kappa^e}{h} 
 \sepr \restr{\kappa}{N} 
 ~\sepr~ N \para N  \\
  r & ::= & \epsilon \sepr (add:\langle Q, T\rangle) \sepr (upd:\mycase{~x~}{T_{i}}{Q_i}{i \in I})
  \end{eqnarray*}
\end{mydef}  
The construct $\new(\gtype{G})$ initializes the global type $\gtype{G}$:   this entails setting up monitored processes in appropriate locations, establishing a session channel $\cha$, and creating   
a message queue $\kappa: h$ for supporting asynchronous among monitored processes.
We write $\emptyset$ to denote 
  the empty message queue; messages 
 are of the form  $(\pt{p}, \pt{q}, \lambda(v))$ thus
 denoting the fact that participant $\pt{p}$ sends value $v$ and label $\lambda$  to  participant $\pt{q}$.
 Message concatenation is denoted with `$\cdot$'.
 
 With respect to the networks in~\cite{CDV15j}, we introduce three new constructs for
active locations, inactive locations, and event queues. 
These are denoted
  $\scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool;\que{\locf{loc}}{r}}$,
  $\scomponent{\locf{loc}}{\Pool;\que{\locf{loc}}{\epsilon}}$,
  and 
  \que{\kappa^e}{h}, respectively. 
We have discussed active locations above;  inactive locations represent 
locations without a monitored process. 
Our model assumes a preexisting set of locations
 which are ``filled in'' with appropriate monitored processes upon initialization of global types.
 The \emph{event queue} \que{\kappa^e}{h} is used to handle internal adaptation requests, associated to the process   $c!(\gtype{G}).P$ introduced earlier.
%  Also, 
% $P$ is a process, $m_P$ is the  monitor associated to $P$,
% $\monpro{m}{P}$ is a monitored process, 
%  and $\Pool$ is a set of pairs $(Q, T_Q)$ of implementations $Q$ and their corresponding type  $T_Q$.

\subsection{Process Types}
%\jp{We need to add a sentence that links the previous section with this one.}
We now proceed to add types to the process language introduced in Definition~\ref{d:processes}.
While in multiparty session types~\cite{DBLP:conf/popl/HondaYC08}, the process types 
 correspond to \emph{local types} (the projection of the global type onto every participant),
the approach developed in~\cite{CDV15j} uses 
a discipline of 
process types which is different from local types (i.e., monitors). This adds flexibility, and is useful to establish an independence between local implementations
(as formalized by processes) and choreographic coordination (as formalized by global types and monitors). Clearly, process types  cannot be completely independent from monitors; a basic consistency between the two should exist. This consistency is defined in terms of \emph{adequacy}, a notion which uses subtyping to determine which process types ``fit'' a given monitor description.

Following~\cite{DBLP:journals/corr/abs-1101-4429}, the process types defined on~\cite{CDV15j} exploit intersection and union types; this ensures an intuitive subtyping relation. Here we consider a syntax for process types that is certainly closer to the local types of~\cite{DBLP:conf/popl/HondaYC08} than the syntax in~\cite{CDV15j}.
This is for the sake of  presentation, as we wish to keep a conceptual relation with the binary session types introduced in~\S\,\ref{s:types}. We then have:

\begin{mydef}[Process Types] The syntax of process types is defined as follows:
\begin{eqnarray*}
{T} & ::= & \&\{\lambda_i(S_i).T_i\}_{i \in I} ~\sepr~ 
		\oplus\{\lambda_i(S_i).T_i\}_{i \in I} 
		 ~\sepr ~ \mu t . T ~\sepr~ t ~\sepr~ \mathsf{end}
\end{eqnarray*}
We write 
$\mathcal{T}$ to denote the set of all types, and use 
${T}, {T}', \ldots$ to range over types.
\end{mydef}

%The framework of~\cite{CDV15j} considers so-called \emph{process types}, a simple typing structure 
%based upon intersection types (intended for external choices),
%union types (intended for internal choices, cf. conditionals),
%and communication types (intended for input and output prefixes).
%Process types are defined by giving a set of \emph{pre-types} which are then
%restricted according to some well-formedness conditions.
%
%\begin{mydef}[Pre-types]
%The set of \emph{pre-types} is inductively defined by
%\begin{eqnarray*}
%T & ::= & ?\lambda(S).T ~\sepr~ !\lambda(S).T ~\sepr~ T \land T ~\sepr~ T \lor T ~\sepr~ \mathsf{end}
%\end{eqnarray*}
%where it is assumed that prefix `\,.\,' has precedence over $\land$ and $\lor$.
%\end{mydef}
%
%The set of pre-types is restricted in order to rule out ambiguous intersection types, i.e.,
%types of the form $T_1 \land T_2$ in which the first action in $T_1$ and $T_2$ is the same but has different continuations.
%Also, the argument of union types is forced to be an output type. 
%These conditions are formalized using the following mappings $\mathbf{lin}$ and $\mathbf{lout}$:
%\begin{eqnarray*}
%\mathbf{lin}(?\lambda(S).T) = \mathbf{lout}(!\lambda(S).T) & = & \lambda \\
%\mathbf{lin}(!\lambda(S).T) = \mathbf{lout}(?\lambda(S).T) & = & \emptyset \\
%\mathbf{lin}(T_1 \land T_2) = \mathbf{lin}(T_1 \lor T_2) & = & \mathbf{lin}(T_1) \cup \mathbf{lin}(T_2) \\
%\mathbf{lout}(T_1 \land T_2) = \mathbf{lout}(T_1 \lor T_2) & = & \mathbf{lout}(T_1) \cup \mathbf{lout}(T_2)
%\end{eqnarray*}
%
%\begin{mydef}[Process Types]
%A \emph{process type} is a pre-type which satisfies the following two conditions, modulo idempotence, commutativity, and
%associativity of unions and intersections:
%\begin{enumerate}[(i)]
%\item All occurrences of the form $T_1 \land T_2$ are such that: 
%$$
%\mathbf{lin}(T_1) \cap \mathbf{lin}(T_2)= \emptyset  = \mathbf{lout}(T_1) \cap \mathbf{lout}(T_2) 
%$$
%\item All occurrences of the form $T_1 \lor T_2$ are such that: 
%$$
%\mathbf{lin}(T_1) = \mathbf{lin}(T_2) = \emptyset = \mathbf{lout}(T_1) \cap \mathbf{lout}(T_2)
%$$
%\end{enumerate}
%We write 
%$\mathcal{T}$ to denote the set of all types, and use 
%$\mathsf{T},\mathsf{T}', \ldots$ to range over types.
%\end{mydef}
Thus, intuitively, 
process types $\&\{\lambda_i(S_i).T_i\}_{i \in I}$
and $\oplus\{\lambda_i(S_i).T_i\}_{i \in I}$
are used to type labelled inputs and outputs, respectively.
Recursive types are as expected, following usual considerations for type equality.

An \emph{environment} $\Gamma$ is a finite mapping from expression variables to sorts and from process variables to types:
$$
\Gamma ::= \emptyset ~\sepr~  \Gamma, x:S ~\sepr~ \Gamma, X: {T} 
$$
where notation $\Gamma, x:S$ (resp. $\Gamma, X:\mathsf{T}$) means that $x$ (resp. $X$) does not occur in the 
domain of $\Gamma$.

We now introduce \emph{typing judgments} for expressions and processes.
Expressions are typed by sorts; the judgment for expression is of the form
$$
\Gamma \vdash e:S
$$
where we assume standard typing rules for expressions.
Judgments for processes are of the form
$$
\multyping{\Gamma}{P}{c:{T}}
$$
which makes it explicit that processes with at most one channel can be typed.
Typing rules for processes are given in Table~\ref{tab:trulesdezani}.
Due to the absence of explicit flags for adaptation, they correspond to a subset of the typing rules given in~\cite{CDV15j}.
We also consider a rule $\rulename{M:Adapt}$ which represents the fact that internal adaptation requests are
defined independently from communication protocols abstracted by types.

\begin{table}%[t]
\[
\begin{array}{c}
\inferrule*[right=\rulename{M:Exp}]{ }{\Gamma,e:S\vdash e:S} 
\qquad 
\inferrule*[right=\rulename{M:End}]{ }{\multyping{\Gamma}{\nil}{c:\mathsf{end}}} 
\qquad 
\inferrule*[right=\rulename{M:Adapt}]{\multyping{\Gamma}{P}{c:{T}}}{
\multyping{\Gamma}{c!(G).P}{c:{T}}}
\qquad 
\inferrule*[right=\rulename{M:Rec}]{\multyping{\Gamma, X:{T}}{P}{c:{T}}}{
\multyping{\Gamma}{\mu\rv{X}.P}{c:{T}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{M:Rcv}]{\multyping{\Gamma, x_1:S_1}{P_1}{c:{T}_1}
\quad \cdots \quad 
\multyping{\Gamma, x_n:S_n}{P_n}{c:{T}_n}
}{
\multyping{\Gamma}{c?\{\lambda_i(x_i).P_i\}_{i \in I}}{c:\&\{\lambda_i(S_i).{T}_i\}_{i \in I}}}
\qquad 
\inferrule*[right=\rulename{M:Send}]{\multyping{\Gamma}{P}{c:{T}_k} \qquad \Gamma \vdash e:S  \qquad k \in I}{
\multyping{\Gamma}{c!\lambda(e).P}{c:\oplus\{\lambda_i(S_i).{T}_i\}_{i \in I}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{M:If}]{\Gamma \vdash e:S  \qquad \multyping{\Gamma}{P_1}{c:{T}} \qquad \multyping{\Gamma}{P_2}{c:{T}} %\qquad {T}_1 \lor {T}_2 \in \mathcal{T}
}{
\multyping{\Gamma}{\ifte{e}{P_1}{P_2}}{c: {T}}}
%\vspace{1.5mm} \\
%\qquad
%\inferrule*[right=\rulename{M:Choice}]{\multyping{\Gamma}{P_1}{c:{T}_1} \qquad \multyping{\Gamma}{P_2}{c:{T}_2} \qquad {T}_1 \land {T}_2 \in \mathcal{T}}{
%\multyping{\Gamma}{P_1+P_2}{c: {T}_1 \land {T}_2 }}
\end{array}
\]
\caption{Typing rules for multiparty processes.} \label{tab:trulesdezani}
\end{table}

The relationship between process types and monitors is formalized via \emph{adequacy}.
Adequacy relies on a subtyping relation, here denoted $\subty$; it corresponds to the 
a finite variant of the subtyping \csub (formally given in Definition~\ref{d:subt}).
Our notion of adequacy is simple, and highlights how the difference between monitors and process types
lies in the information about participant identities.

%\red{qui pensavi di omettere completamente la definizione di subtyping?}
% on process types, defined next. 
%The relation $\subty$ is defined as the smallest reflexive, transitive relation on $\mathcal{T}$ such that 
%\begin{eqnarray*}
%\mathsf{T} & \subty &  \mathsf{end}  \\
%\mathsf{T}_1 \land \mathsf{T}_2 & \subty & \mathsf{T}_i  \quad (i \in \{1,2\}) \\
%\mathsf{T}_i & \subty & \mathsf{T}_1 \lor \mathsf{T}_2  \quad (i \in \{1,2\}) \\
%\mathsf{T}_1 \subty \mathsf{T}_2 & \Rightarrow & !\lambda(S).\mathsf{T}_1 \subty !\lambda(S).\mathsf{T}_2 \\
%\mathsf{T}_1 \subty \mathsf{T}_2 & \Rightarrow &  ?\lambda(S).\mathsf{T}_1 \subty ?\lambda(S).\mathsf{T}_2 \\
%(\mathsf{T} \subty \mathsf{T}_1 \& \mathsf{T} \subty \mathsf{T}_2) & \Rightarrow &
%\mathsf{T} \subty \mathsf{T}_1 \land \mathsf{T}_2 \\
%(\mathsf{T}_1 \subty \mathsf{T} \& \mathsf{T}_2 \subty \mathsf{T}) & \Rightarrow  & 
%\mathsf{T}_1 \lor \mathsf{T}_2 \subty\mathsf{T} \\
%(\mathsf{T}_1 \lor \mathsf{T}_2)  \land \mathsf{T}_3 \subty \mathsf{T} & \Leftrightarrow & 
%(\mathsf{T}_1 \land \mathsf{T}_3  \subty \mathsf{T}) \& (\mathsf{T}_2 \land \mathsf{T}_3  \subty \mathsf{T}) \\
%\mathsf{T}  \subty (\mathsf{T}_1 \land \mathsf{T}_2) \lor \mathsf{T}_3 & \Leftrightarrow & 
%(\mathsf{T}  \subty \mathsf{T}_1 \lor \mathsf{T}_3 \& \mathsf{T}  \subty \mathsf{T}_2 \lor \mathsf{T}_3)
%\end{eqnarray*}
%Intuitively, if $\mathsf{T}_1  \subty \mathsf{T}_2$ then 
%$\mathsf{T}_1$ has all the behaviors specified by $\mathsf{T}_2$ but possibly more.
%Subtyping is decidable; see~\cite{CDV15j} for details.
%We are now ready to define adequacy:


\begin{mydef}[Adequacy]
Let $|\cdot|$ be a mapping from monitors to types defined as follows:
\begin{eqnarray*}
 |\pt{p}?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} | & = & \&\{ \lambda_i(S_i).\,|\moni{M}_i| \}_{i \in I}\\
  |\pt{p}!\{\lambda_i(S_i).\moni{M}_i\}_{i\in I}| & = & \oplus\{\lambda_i(S_i).\,|\moni{M}_i|\}_{i \in I}\\
  |\mathsf{end}| & = & \mathsf{end}
\end{eqnarray*}
We then say that type ${T}$ is \emph{adequate}  to monitor $\moni{M}$ (notation ${T} \propto \moni{M}$) if ${T} \subty |\moni{M}|$.
\end{mydef}



\subsection{Semantics}
We now move on to formalize the semantics of networks (cf. Definition \ref{d:networks}) 
in terms of a reduction relation, denoted  $N\pired N'$. 
We require some auxiliary definitions, in order to connect the behavior of monitors and processes to that of whole networks;
we also require a structural congruence to capture, among other things, asynchronous message communication
as handled via queues. 
As in~\cite{CDV15j}, we assume that all local collections $\Pool$ are \emph{complete}, which intuitively means that 
such collections contain
all conceivable  pairs of types and processes. 

Reduction for networks relies on labeled transition systems (LTS) for monitors and processes.
%\paragraph{LTS for Monitors and Processes}
The LTS for monitors is rather simple; it is used to enable the actions to be performed by processes:
%To that end, the semantics of networks relies on the following LTS on monitors:
$$
\pt{p}?\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} \xrightarrow{\pt{p}?\lambda_j} \moni{M}_j \quad (j \in I)
\qquad \qquad
\pt{q}!\{\lambda_i(S_i).\moni{M}_i\}_{i\in I} \xrightarrow{\pt{q}!\lambda_j}  \moni{M}_j \quad (j \in I)$$

%\paragraph{LTS for Processes}
The LTS for processes  relies on the following set of 
labels, with associated
rules as in 
in Table~\ref{tab:ltsprocdezani}.
$$
\alpha ::= \tau \sepr  \kappa[\pt{p}]?\lambda(v) \sepr \kappa[\pt{p}]!\lambda(v) \sepr \kappa[\pt{p}]!\lambda(G)
$$
%and internal and global adaptation actions:
%$$
%\delta ::= \tau \sepr \kappa[p]!\lambda(G)
%$$
%\jp{Question: probably $\kappa[p]!\lambda(G)$ should be in $\alpha$?}
%The distinction is meant to formalize the fact that communication actions (sessions) are independent from other kinds of actions. 


\begin{table}%[t]
\begin{center}
 

\[
\begin{array}{c}
\inferrule*[right=\rulename{M:P:In}]{ }{\kappa[\pt{p}]?\{\lambda_i(x_i).P_i\}_{i \in I} \xrightarrow{\kappa[\pt{p}]?\lambda_j(v_j)} P_j \subst{v}{x}} 
\qquad 
\inferrule*[right=\rulename{M:P:Out}]{e \leadsto v }{\kappa[\pt{p}]!\lambda(e).P \xrightarrow{\kappa[\pt{p}]!\lambda(v)} P}  
\vspace{2mm} \\
\inferrule*[right=\rulename{M:P:AdapOut}]{ }{\kappa[\pt{p}]!\lambda(G).P \xrightarrow{\kappa[p]!\lambda(G)} P} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{M:P:IfT}]{e \leadsto \mathtt{true}  }{\ifte{e}{P_1}{P_2} \xrightarrow{\tau} P_1} 
\qquad 
\inferrule*[right=\rulename{M:P:IfF}]{e \leadsto \mathtt{false}  }{\ifte{e}{P_1}{P_2} \xrightarrow{\tau} P_2} 
\qquad 
\inferrule*[right=\rulename{M:P:Rec}]{ }{\mu\rv{X}.P \xrightarrow{\tau} P\subst{\mu\rv{X}.P}{X}} 
%\vspace{1.5mm} \\
%\inferrule*[right=\rulename{M:P:ChoVis}]{P \xrightarrow{\alpha} P'}{
%P + Q \xrightarrow{\alpha} P'}
%\qquad
%\inferrule*[right=\rulename{M:P:ChoInt}]{P \xrightarrow{\delta} P'}{
%P + Q \xrightarrow{\delta} P' + Q}
\end{array}
\]
\end{center}

\caption{LTS for multiparty processes.} \label{tab:ltsprocdezani}
\end{table}


%\paragraph{Equivalence for Networks and Queues}
Reduction for networks relies also on a \emph{structural equivalence} and on
\emph{evaluation contexts}. 
The structural equivalence on networks, denoted $\equiv$, 
defines 
parallel composition as a communicative, associative operator, and which 
allows restriction to reduce and enlarge their scope without name clashes. 
Also, it decrees that any monitored process with the $\mathsf{end}$ monitor corresponds to the neutral element for parallel composition
and absorbs restriction. More formally:
\begin{eqnarray*}
\monpro{\mathsf{end}}{P} \para N \equiv N 
\qquad
\restr{\kappa}{\monpro{\mathsf{end}}{P}} \equiv \monpro{\mathsf{end}}{P}
\qquad 
\restr{\kappa}{N_1} \para N_2 \equiv \restr{\kappa}{N_1 \para N_2}
\\\
\restr{\kappa}{(\kappa:h)} \para N \equiv N 
\qquad 
\restr{\kappa}\restr{\kappa'}{N} \equiv \restr{\kappa'}\restr{\kappa}{N}
\end{eqnarray*}
We consider also an structural equivalence for message queues which allows us to  
commute  messages involving different receivers or senders:
%and (ii)~splits a message to multiple receivers:
\begin{eqnarray*}
h \cdot (\pt{p}, \pt{q}, \lambda_i(v_i)) \cdot (\pt{p}', \pt{q}', \lambda_j(v_j)) \cdot h' & \equiv & 
h \cdot  (\pt{p}', \pt{q}', \lambda_j(v_j)) \cdot  (\pt{p}, \pt{q}, \lambda_i(v_i)) \cdot h' \qquad \text{if $\pt{p} \neq \pt{p}'$ or $\pt{q} \neq \pt{q}'$} 
%h \cdot (q, \Pi, \lambda(v))  \cdot h' & \equiv & 
%h \cdot (q, \Pi_1, \lambda(v)) \cdot (q, \Pi_2, \lambda(v)) \cdot h' \qquad \text{if $\Pi = \Pi_1 \cup \Pi_2$ and $\Pi_1 \cap \Pi_2 = \emptyset$ }
\end{eqnarray*}
This congruence is extended for networks in the expected way by letting:
$$h \equiv h'  \text{ implies } \kappa: h \equiv \kappa: h'$$ 

%\paragraph{Reduction Semantics for Networks.}

Finally, we have the following definition for evaluation contexts, denoted $\mathcal{E}$:
%\begin{mydef}
% An evaluation context is:
 $$
 \mathcal{E}::= [~] ~\sepr~ \mathcal{E} \para N ~\sepr~ 
 \restr{\kappa}{\mathcal{E}}
 $$
%\end{mydef}

%
%  OLD REDUCTION RULES 
%\begin{table}
% \[
% \begin{array}{c}
% \inferrule*[right=\rulename{N:Open}]{\Pi = \pa(G) \\ \forall p \in \Pi~  (p \in \locf{loc}_p\\ (P_p, T_p) \in \Pool_p \\ \moni{M}_p = G \downarrow p \\ T_p \propto \moni{M}_p)} 
%           {\new(G) \para \prod_{p \in \Pi} \scomponent{\locf{loc}_p}{\Pool_p;\,\que{\locf{loc}_p}{\epsilon}}  \pired \restr{\kappa}{(\prod_{p \in \Pi} \scomponent{\locf{loc}_p}{\monpro{\moni{M}_p}{P_p\subst{\kappa[p]}{y}};\,\Pool_p;\,\que{\locf{loc}_p}{\epsilon}} \para  \kappa: \emptyset \para \que{\kappa^e}{\epsilon} ) } }
%\vspace{2mm}\\
%
%\inferrule*[right=\rulename{N:Send}]
%{\moni{M} \xrightarrow{q!\lambda} \moni{M}' \\ 
% P \xrightarrow{\kappa[p]!\lambda(v)} P'}
%{ \scomponent{\locf{loc}_p}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}_p}{\epsilon}} \para  \kappa: h \para \que{\kappa^e}{\epsilon} \pired
%\scomponent{\locf{loc}_p}{\monpro{\moni{M}'}{P'};\,\Pool;\,\que{\locf{loc}_p}{\epsilon}} \para  \kappa: (p,q,\lambda(v))\cdot h \para \que{\kappa^e}{\epsilon}
%}
%\vspace{2mm}\\
%
%\inferrule*[right=\rulename{N:Rcv}]
%{\moni{M} \xrightarrow{q?\lambda} \moni{M}' \\ 
% P \xrightarrow{\kappa[p]?\lambda(v)} P'}
%{ \scomponent{\locf{loc}_p}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}_p}{\epsilon}} \para  \kappa: (q,p,\lambda(v))\cdot h \para \que{\kappa^e}{\epsilon} \pired
%\scomponent{\locf{loc}_p}{\monpro{\moni{M}'}{P'};\,\Pool;\,\que{\locf{loc}_p}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon}
%}
%\vspace{2mm}\\
%
%\inferrule*[right=\rulename{N:Tau}]
%{
% P \xrightarrow{\tau} P'}
%{ \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon} \pired
%\scomponent{\locf{loc}}{\monpro{\moni{M}}{P'};\,\Pool;\,\que{\locf{loc}}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon}
%}
%\vspace{2mm}\\
%
%\inferrule*[right=\rulename{N:Inmsg}]{\kappa!(G).P \xrightarrow{\kappa!(G)} P}
%                 {\scomponent{\locf{loc}}{\monpro{\moni{M}}{\kappa!(G).P};\Pool;\que{\locf{loc}}{\epsilon}} \para \que{\kappa^e}{\epsilon} \para \kappa:h 
%                 \pired 
%               \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool;\que{\locf{loc}}{\epsilon}} \para \que{\kappa^e}{G} \para \kappa:h } \\
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%\inferrule*[right=\rulename{N:InUpd}]{
%    1) p \in \pa(G) \cap \pa(G') \quad \moni{M}_p' = G'  \downarrow p = \moni{M}_p \quad P_p'= P_p \\
%    2)  p \in \pa(G) \cap \pa(G') \quad \moni{M}_p' = G'  \downarrow p \neq \moni{M}_p \quad (P_p',T_p) \in \Pool_{p} \quad T_p \propto \moni{M}'_p   \\
%    3)  p \in \pa(G') \setminus \pa(G) \quad (P_p, T_p) \in \Pool_p \quad  \moni{M}_p' = G'  \downarrow p \quad T_p \propto \moni{M}'_p \quad P'_P = P_P\subst{\kappa[p]}{y}
%}
%{
%%\begin{array}{c}
%\prod_{q \in \pa(G') \setminus \pa(G)} \scomponent{\locf{loc}_q}{\Pool_q;\que{\locf{loc}_q}{\epsilon}} \para 
%                 \restr{\kappa}{(\prod_{p \in \pa(G)} \scomponent{\locf{loc}_p}{\monpro{\moni{M}_p}{P_p};\Pool_p;\que{\locf{loc}_p}{\epsilon}} \para  \kappa:h \para \que{\kappa^e}{G'} )} \\  \pired  
%                 \restr{\kappa}{(\prod_{p \in \pa(G')} \scomponent{\locf{loc}_p}{\monpro{\moni{M}'_p}{P'_p};\Pool_p;\que{\locf{loc}_p}{\epsilon}} \para \kappa:\epsilon \para \que{\kappa^e}{\epsilon} )} \para  \prod_{q \in \pa(G) \setminus \pa{G'}} \scomponent{\locf{loc}_q}{\Pool_q;\que{\locf{loc}_q}{\epsilon}}                  }
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
% \inferrule*[right=\rulename{N:Addloc1}]{\exists (R, T_R) \in \Pool \quad T_R \leq T_Q}
%{\scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool; \que{\locf{loc}}{(add:\langle Q, T_Q\rangle)}} \pired \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool \cup \{(Q, T_{Q})\} \setminus \{(R, T_R)\}; \que{\locf{loc}}{\epsilon} }}
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
% \inferrule*[right=\rulename{N:Addloc2}]{\exists (R, T_R) \in \Pool \quad T_R \leq T_Q}
%{\scomponent{\locf{loc}}{\Pool; \que{\locf{loc}}{(add:\langle Q, T_Q\rangle)}} \pired \scomponent{\locf{loc}}{\Pool \cup \{(Q, T_{Q})\} \setminus \{(R, T_R)\}; \que{\locf{loc}}{\epsilon} }}
%\vspace{2mm}\\
%
% \inferrule*[right=\rulename{N:Updloc}]{\exists j \in I \quad \moni{M} \propto T_i}{\scomponent{\locf{loc_p}}{(\monpro{\moni{M}}{P};\Pool; \que{\locf{loc}_p}{(upd:\mycase{~x~}{\T_{i}}{Q_i}{i \in I})}} \pired \scomponent{\locf{loc}_p}{\monpro{\moni{M}}{Q_j\subst{\kappa[p]}{y}};\Pool; \que{\locf{loc}_p}{\epsilon}}}
%\vspace{2mm}\\
%
%\inferrule*[right=\rulename{N:Equiv}]
%{N_1\equiv N_1' \\ N_1 \pired N_2 \\ N_2 \equiv N_2'}
%{N_1' \pired N_2'}
%\qquad
%\inferrule*[right=\rulename{N:Eval}]
%{  N\pired N' }
%{\eval{N} \pired \eval{N'}}
%
%
%
%\end{array}
%\]
% \caption{LTS for networks.} \label{tab:ltsnetworksold}
%\end{table}


\begin{table}%[h!]
\[
\begin{array}{lc}
 \rulename{N:Open} & 
 \displaystyle \frac{\Pi = \pa(\gtype{G}) \qquad \forall \pt{p} \in \Pi.\big(\moni{M}_\pt{p} = \proje{\gtype{G}}{\pt{p}}\,\land\, (P_\pt{p}, T_\pt{p}) \in \Pool_\pt{p}   \,\land\,   T_\pt{p} \propto \moni{M}_\pt{p}   \,\land\, \mathcal{L}_{\gtype{G}}(\pt{p}) = \locf{loc}_\pt{p} \big)} 
           {\displaystyle\new(\gtype{G}) \para \prod_{\pt{p} \in \Pi} \scomponent{\locf{loc}_\pt{p}}{\Pool_\pt{p};\,\que{\locf{loc}_\pt{p}}{\epsilon}}  \pired \restr{\kappa}{(\prod_{\pt{p} \in \Pi} \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}_\pt{p}}{P_\pt{p}\subst{\kappa[\pt{p}]}{y}};\,\Pool_\pt{p};\,\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa: \emptyset \para \que{\kappa^e}{\epsilon} ) } } 
\vspace{2mm}           \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{N:Send} & 
\displaystyle \frac{\moni{M} \xrightarrow{\pt{q}!\lambda} \moni{M}' \qquad 
 P \xrightarrow{\kappa[\pt{p}]!\lambda(v)} P'}
{ \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa: h \para \que{\kappa^e}{\epsilon} \pired
\scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}'}{P'};\,\Pool;\,\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa: (\pt{p},\pt{q},\lambda(v))\cdot h \para \que{\kappa^e}{\epsilon}
}
\vspace{2mm}           \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{N:Recv} & 
\displaystyle \frac{\moni{M} \xrightarrow{\pt{q}?\lambda} \moni{M}' \qquad 
 P \xrightarrow{\kappa[\pt{p}]?\lambda(v)} P'}
{ \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa: (\pt{q},\pt{p},\lambda(v))\cdot h \para \que{\kappa^e}{\epsilon} \pired
\scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}'}{P'};\,\Pool;\,\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon}
}
\vspace{2mm}           \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{N:Tau} &
\displaystyle \frac{
 P \xrightarrow{\tau} P'}
{ \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\,\Pool;\,\que{\locf{loc}}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon} \pired
\scomponent{\locf{loc}}{\monpro{\moni{M}}{P'};\,\Pool;\,\que{\locf{loc}}{\epsilon}} \para  \kappa:  h \para \que{\kappa^e}{\epsilon}
}
\vspace{2mm}           \\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{N:InMsg} &
\displaystyle \frac{P \xrightarrow{\kappa!(\gtype{G})} P'}
                 {\scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool;\que{\locf{loc}}{\epsilon}} \para \que{\kappa^e}{\epsilon} \para \kappa:h 
                 \pired 
               \scomponent{\locf{loc}}{\monpro{\moni{M}}{P'};\Pool;\que{\locf{loc}}{\epsilon}} \para \que{\kappa^e}{\gtype{G}} \para \kappa:h }
               
               \vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\rulename{N:InUpd} & 
\displaystyle \frac{
\begin{array}{ccl}
%\pa(\gtype{G}) = \Pi \qquad 
\pa(\gtype{G}') = \Pi' &    & 
    \forall \pt{p} \in \Pi'. \big(
        (\pt{p} \in \Pi \cap \Pi' \,\land\, \proje{\gtype{G}'}{\pt{p}}  = \moni{M}_\pt{p} = \moni{M}'_\pt{p} \,\land\, P'_\pt{p}= P_\pt{p} )~ \lor 
     \\
       & & \qquad  (\pt{p} \in \Pi \cap \Pi' \,\land\, \proje{\gtype{G}'}{\pt{p}}  = \moni{M}'_p \neq \moni{M}_\pt{p} \,\land\, 
        (Q_\pt{p},T_\pt{p}) \in \Pool_{\pt{p}} \,\land\,
        T_\pt{p} \propto \moni{M}'_{\pt{p}} \,\land\, P'_\pt{p} = Q_\pt{p}\subst{\kappa[\pt{p}]}{y} )~ \lor  \\
       & & \qquad (\pt{p} \in \Pi' \setminus \Pi \,\land\,  (Q_\pt{p}, T_\pt{p}) \in \Pool_\pt{p} \,\land\, \proje{\gtype{G}'}{\pt{p}}  = \moni{M}'_\pt{p} \,\land\, T_\pt{p} \propto \moni{M}'_\pt{p} \,\land\, P'_\pt{p} = Q_\pt{p}\subst{\kappa[\pt{p}]}{y}) \big) \\
%            2)  p \in \pa(\gtype{G}) \cap \pa(\gtype{G}') \quad \moni{M}_p' = \gtype{G}'  \downarrow p \neq \moni{M}_p \quad (P_p',T_p) \in \Pool_{p} \quad T_p \propto \moni{M}'_p   \\
%    3)  p \in \pa(\gtype{G}') \setminus \pa(\gtype{G}) \quad (P_p, T_p) \in \Pool_p \quad  \moni{M}_p' = \gtype{G}'  \downarrow p \quad T_p \propto \moni{M}'_p \quad P'_P = P_P\subst{\kappa[p]}{y}
    \end{array}
}
{
\begin{array}{c}\displaystyle 
\restr{\kappa}{\big(\prod_{\pt{p} \in \Pi} \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}_\pt{p}}{P_\pt{p}};\Pool_\pt{p};\que{\locf{loc}_\pt{p}}{\epsilon}} \para  \kappa:h \para \que{\kappa^e}{\gtype{G}'}\big)} 
\para
\prod_{\pt{q} \in \Pi' \setminus \Pi} \scomponent{\locf{loc}_\pt{q}}{\Pool_\pt{q};\que{\locf{loc}_\pt{q}}{\epsilon}}  
                 \\  \pired  \\ \displaystyle 
                 \restr{\kappa}{\big(\prod_{\pt{p} \in \Pi'} \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}'_\pt{p}}{P'_\pt{p}};\Pool_p;\que{\locf{loc}_\pt{p}}{\epsilon}} \para \kappa:\epsilon \para \que{\kappa^e}{\epsilon} \big)} \para  \prod_{\pt{q} \in \Pi \setminus \Pi'} \scomponent{\locf{loc}_\pt{q}}{\Pool_\pt{q};\que{\locf{loc}_\pt{q}}{\epsilon}}                  
                 \end{array}
                 }
\vspace{2mm}\\
\rulename{N:Addloc1} & 
\displaystyle\frac{\exists (R, T_R) \in \Pool \qquad T_R \leq T_Q \qquad \Pool' = \Pool \cup \{(Q, T_{Q})\} \setminus \{(R, T_R)\}}
{\scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool; \que{\locf{loc}}{(add:\langle Q, T_Q\rangle)}} \pired \scomponent{\locf{loc}}{\monpro{\moni{M}}{P};\Pool'; \que{\locf{loc}}{\epsilon} }}
\vspace{2mm}\\
\rulename{N:Addloc2} & 
\displaystyle\frac{\exists (R, T_R) \in \Pool \qquad T_R \leq T_Q \qquad \Pool' = \Pool \cup \{(Q, T_{Q})\} \setminus \{(R, T_R)\}}
{\scomponent{\locf{loc}}{ \Pool; \que{\locf{loc}}{(add:\langle Q, T_Q\rangle)}} \pired \scomponent{\locf{loc}}{\Pool'; \que{\locf{loc}}{\epsilon} }}
\vspace{2mm}\\
\rulename{N:Updloc} & 
\displaystyle\frac{
(V = P) ~~\lor~~ \exists l \in I. (\mathsf{match}^\propto_I(l, \{\moni{M}\}, \{T_i\}_{i \in I}) \land R = Q_l\subst{\kappa[\pt{p}]}{y})
}{\scomponent{\locf{loc}_\pt{p}}{(\monpro{\moni{M}}{P};\Pool; \que{\locf{loc}_\pt{p}}{(upd:\mycase{x}{T_{i}}{Q_i}{i \in I})}} \pired \scomponent{\locf{loc}_\pt{p}}{\monpro{\moni{M}}{R};\Pool; \que{\locf{loc}_\pt{p}}{\epsilon}}}
\vspace{2mm}\\
\rulename{N:Equiv} & 
\displaystyle\frac{N_1\equiv N_1' \qquad N_1 \pired N_2 \qquad  N_2 \equiv N_2'}
{N_1' \pired N_2'}
\vspace{2mm}\\
\rulename{N:Eval} & 
\displaystyle\frac{  N\pired N' }
{\eval{N} \pired \eval{N'}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 \end{array}
\]
\caption{Reduction Semantics for Multiparty Processes.
\label{tab:ltsnetworks}}
\end{table}

\bigskip

\noindent The rules of the reduction semantics for networks are given in Table~\ref{tab:ltsnetworks};
we now describe them:
\begin{enumerate}[$-$]
\item Rule \rulename{N:Open}
initializes a global type, denoted $\gtype{G}$ in the rule.
To that end, it considers all the inactive locations associated to the declared participants of $\gtype{G}$, denoted $\Pi$.
For each participant $\pt{p}$, a process implementation is picked up from the local collection $\Pool_\pt{p}$.
The process type of this implementation is expected to be adequate to the monitor, defined by $\proje{\gtype{G}}{\pt{p}}$.
Observe that mapping $\mathcal{L}_\gtype{G}$ ensures that each participant is assigned to a different (inactive) location.
A fresh session name $\cha$ is created for protocol participants; associated message and event queues are also created.
%the set up of a multiparty session consists in selecting a proper (type-compatible) participant in a given location from a set of possible implementations $\mathcal{P}$. Only one participant per location can be chosen. 

\item Rules \rulename{N:Send} and \rulename{N:Recv} regulate output and input actions from/to the message queue of an already established session. Observe how the action must be enabled by the label of the monitor, which also describes information on the receiver/sender of the exchanged value. Both monitors and processes evolve as a result of the interaction with the queue. In both rules, a reduction is enabled provided the event queue is empty. Rule \rulename{N:Tau} formalizes the fact that evaluation of conditional expressions and recursion unfolding within a (monitored) process can occur without affecting its monitor. 

%\paragraph{Internal Adaptation.}
\item Rules \rulename{N:InMsg} and \rulename{N:InUpd}
formalize \emph{internal adaptation}.
Similarly as rule \rulename{N:Tau}, 
issuing an internal adaptation request 
is a behavior specified by the process but independent from its monitor.
Rule \rulename{N:InMsg} is enabled if the event queue is empty; its main 
consequence is the addition of a global type to the event queue of the session. 

Once a global type is added to the event queue, rule \rulename{N:InUpd} can be triggered. 
This rule assumes that a fixed set of participants (denoted $\Pi$ in the rule) is already executing a global protocol
and should adapt to execute a new global protocol.
This protocol is denoted $\gtype{G}'$ in the rule; it has a set of participants denoted $\Pi'$.
The rule sets up local implementations for all participants in $\Pi'$, also considering 
the existing behaviors in the set of participants $\Pi$. There are three possibilities:
\begin{enumerate}
\item Participant $\pt{p}$ belongs to both $\Pi$ and $\Pi'$ and location $\locf{loc}_{\pt{p}}$ encloses a monitored
process that ``fits'' with the projection of $\gtype{G}'$ onto $\pt{p}$. In this case, the monitored process
is kept as it is. 

\item Participant $\pt{p}$ belongs to both $\Pi$ and $\Pi'$,
but the current monitored process enclosed in 
 location $\locf{loc}_{\pt{p}}$ is not compatible with the projection of $\gtype{G}'$ onto $\pt{p}$. In this case,
 a new process implementation is selected from the local collection $\Pool_\pt{p}$ and instantiated with an appropriate session name.
 
 \item  Participant $\pt{p}$ belongs to $\Pi'$ but not to $\Pi$. In this case, the respective location 
 is made active by setting up an appropriate monitored process extracted from the collection.
 
  
\end{enumerate}
These  possibilities are formalized as a disjunction in the premise of rule \rulename{N:InUpd}.
Notice that the left-hand side of the rule considers a series of active locations
(for participants in $\Pi$) together with a series of inactive locations, corresponding to participants 
in $\Pi'$ but not in $\Pi$, i.e., the locations that will become active as a result of the reduction step (cf. item (c) above). Similarly, the right-hand side of the rule features a set of inactive locations, corresponding to   
participants present in $\Pi$ but not in $\Pi'$; i.e., the excluded participants   as a result of the adaptation step.
Also, observe that both message and event queues are emptied after reduction.



 

%\item \rulename{Inupd}: Queue $\que{\kappa^e}{}$ is used to receive the internal updates events. An event basically consists in the new protocol $\gtype{G}'$ that has to replace $\gtype{G}$ \jp{OK, but how do we remember that we are running $G$??}. The application of an internal update empties the session queue $\que{\kappa}{}$ and depending on the role of each  participant has a different behavior:
%\begin{enumerate}
% \item $p$ is a participant of $\gtype{G}'$ that was present in $\gtype{G}$ as well and whose local protocol remains unchanged. In this case nothing changes for the process implementing the protocol of $p$
%  
% \item $p$ is a participant of $\gtype{G}'$ that was present in $\gtype{G}$ and whose local protocol has changed. In this case a new implementation respecting the protocol is chosen in the pool of processes of the location hosting the participant.
% 
% 
% \item $p$ is a new participant (i.e., $p$ did not participate to $\gtype{G}$) in this case we add the corresponding location to the session group of processes
% 
%\end{enumerate}
%Also, all participants $q$ that have been excluded from the protocol $\gtype{G}'$ are moved outside the restriction and the remainder process $P_q$ together with its monitor is deleted. 

%\paragraph{External Adaptation}

\item Rules \rulename{N:Addloc1}, \rulename{N:Addloc2}, and \rulename{N:Updloc}
formalize \emph{external adaptation}.
These rules are enabled by the addition of an adaptation request in the queue of a location. 
Such a request is meant to come from the context of a location, and contains
typed processes.
Rule~\rulename{N:Addloc1} essentially upgrades a process pair present in the 
local collection of an active location; this collection is denoted $\Pool_{\pt{p}}$ in the rule.
Rule~\rulename{N:Addloc2} is similar but applies to inactive locations.
Since we assume that the collection is complete, rules~\rulename{N:Addloc1} and~\rulename{N:Addloc2} implement a form of upgrade operation on the local collection. 

In contrast, rule~\rulename{N:Updloc} formalizes type-directed adaptation for the monitored process, in the spirit of the adaptation mechanism developed for binary sessions. In this case, the external adaptation message contains a finite series of possibilities for refining the current behavior of the monitored process. 
The rule tries to find a compatible update; 
%, i.e., the adaptation routine substitutes $P$ with a process $Q_i$ that has the same behavior of $P$ (up to subtyping)
if no compatible update is present the external request is dismissed, and the monitored process is kept unchanged.
Notice that compatibility depends on a
match predicate,
denoted $\mathsf{match}^\propto_I(l, \{\moni{M}\}, \{T_i\}_{i \in I})$ in the rule.
This predicate is the variation of the predicate given in Definition~\ref{d:matchp} that considers
monitors and process types instead of binary session types, and 
adequacy rather than subtyping.

\item Rules \rulename{N:Equiv} and \rulename{N:Eval} 
define self-explanatory treatments for 
incorporating structural equivalence and evaluation contexts into reduction.  

%\item \rulename{Addloc}: Queue $loc$ has received from the environment the message $add$ together with the implementation and corresponding type $T_Q$ of a program $Q$. Since we assume that the pool is complete, this kind of update actually upgrades a process in the pool by changing its implementation.
%
%
%
%\item \rulename{updloc}: upon reception of an event of external adaptation of kind $upd$ the semantics looks for a compatible update, i.e., the adaptation routine substitutes $P$ with a process $Q_i$ that has the same behavior of $P$ (up to subtyping)
%If no compatible update is present the event is dismissed leaving  the monitored processes unchanged.
%We use the match predicate (Definition~\ref{d:matchp}) using adequacy rather than subtyping.
%\jp{Does it make sense that internal updates have influence over the whole choreography, whereas external updates only have influence in a single participant? Cinzia: I think so}

\end{enumerate}


\begin{myremark}[Adaptation Functions]
We have proposed using processes communicating global types (here denoted 
$c!\lambda(G).P$), rather than adaptation flags, to specify internal adaptation, i.e., adaptation requests issued by the system itself. This is a simple way of formalizing this important class of adaptation routines. As an alternative, a less direct mechanism would consist in communicating a value 
on which a future adaptation should depend on, rather than the expected new choreography. Such a value could be used as a parameter for the adaptation functions used in~\cite{CDV15j}. This would add flexibility to the specification of internal adaptation requests. %; such an adaptation value could even be considered together with the global state of the system
\end{myremark}

Having introduced networks and their semantics, we now proceed to investigate correctness results for them.


\input{multiparty}


%\section{Discussion: A Compartmentalized Model of  Communication and Adaptation}\label{s:compart} 
%Giv\-en that 
%the process model in \S\,\ref{s:evadap}
%enables the interplay of communication and adaptation, 
%how can we organize specifications to 
%reflect a desirable separation of concerns?
%%achieve modular treatment of runtime adaptation? 
%In ongoing work, 
%with the aim of specifying systems at a high-level of abstraction,
%we have developed a model which defines \emph{compartments} to
%isolate communication behavior and adaptation routines. 
%Here we briefly describe this model, which is 
%given in Table~\ref{t:model}.\looseness=-1
%
%In a nutshell, programs of \S\,\ref{s:evadap} are now organized into \emph{systems}. A system $G$
%is the composition of a set  of \emph{applications} $A_1, \ldots, A_n$ each comprising three   elements: 
%a \emph{behavior} $R$, a \emph{state} $\mathsf{S}$, and a \emph{manager} $\mathcal{M}$. 
%As a simple example of a system, we may consider the operating system of a smartphone, which is meant to manage a number of applications that may interact among them.
%%In fact, a
%Applications in our model can communicate between each other %(as in the interaction of different apps) 
%or exhibit intra-application communication. %(as in an app with several modules). 
%The behavior $R$ is specified as a process; 
%we distinguish between located processes representing service definitions  
%from located processes which make use of such definitions. % (the latter are denoted $\scomponentbig{\locf{loc}}{P^{-}}$ in Table~\ref{t:model}).
%A reduction semantics (omitted) ensures that locations enclosing service definitions do not contain open (active) sessions. 
%This may be convenient for defining adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. 
%The state $\mathsf{S}$ collects
%session monitors and location queues and it is kept separate from $R$.  
%As a simple example, the buyer-seller scenario given in \S\,\ref{s:intro} 
%can be casted in our model as 
%\[
% \myapp{\mathsf{byr}}{\scomponentbig{\locf{buyer}}{\,  \nopenr{u@\mathsf{slr}}{x:\ST}.P}}{\mathsf{S_b}}{\mathcal{M}_b} \appar
%\myapp{\mathsf{slr}}{\scomponentbig{\locf{seller}}{ \repopen{u}{y{:}\STT}.Q}}{\mathsf{S_s}}{\mathcal{M}_s} 
%\]
%That is, buyer   and seller  are implemented as  separate applications, named $\mathsf{byr}$  and $\mathsf{slr}$, respectively.
%Above, we have $\mathsf{S_b} = \que{\locf{buyer}}{\epsilon}$   and 
%$\mathsf{S_s} = \que{\locf{seller}}{\epsilon}$.
%
%%In the smartphone scenario, the state roughly corresponds to the set of buffers available for each app.
%While the manager $\mathcal{M}$
%implements adaptation  at the application (local) level,
%a \emph{handler} $\mathcal{H}$ defines adaptation at the 
%system (global) level.
%As we wish to describe communication behavior separately from adaptation routines, 
%update processes are confined to handlers and managers.
%A manager is  meant to react upon the arrival of an internal adaptation message $\mathtt{upd}_I$. 
%As in~\S\,\ref{s:evadap},
%managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).
%A handler  may either  $\mathtt{upd}$ate 
%or  $\mathtt{upg}$rade
%the behavior at some location $\locf{loc}$ within application $a$; this is written $\locf{loc}@a$.
%Upgrades are
%denoted $\nupgbig{\locf{l}_1}{P}$; they are a particular form of update 
%intended for service definitions only. 
%In Table~\ref{t:model} we write $\ast\ift{e}{P}$ and $\repopen{u}{x{:}\ST}.P$ as shorthands for persistent conditionals and services, respectively.
%\begin{table}%[!t]
%\begin{eqnarray*}
%G & ::= & A \sepr \mathcal{H} \sepr \restr{\cha}{A} \sepr G_1 \appar G_2 \sepr \mathbf{0} \qquad \quad
%A  :: =  \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
%%g & :: = & \arrive{\locf{l}@a, \mathtt{upd}_E} \sepr g_1 \land g_2 \sepr g_1 \lor g_2\\
%\mathcal{H} & ::= & 
%*\,\ift{\arrive{\locf{l}_1@a, \mathtt{upd}_E}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \\
%& \sepr & *\,\ift{\arrive{\locf{l}_1@a, \mathtt{upg}}}{\nupgbig{\locf{l}_1}{P}} 
%\\
%R & ::= & \scomponentbig{\locf{loc}}{\nopena{u}{x{:}\ST}.P}   \sepr  \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
%\mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} %\sepr \que{a}{\til{r}}  
%\sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \sepr \mathbf{0} \\
%\mathcal{M} & ::= & *\,\ift{\arrive{\locf{l}_1, \mathtt{upd}_I}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \sepr  \mathcal{M}_1 \mapar \mathcal{M}_2   \sepr \mathbf{0}
%%& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
%\end{eqnarray*}
%%\vspace{-3mm}
%\caption{A Compartmentalized Model of Communicating Systems: Syntax.\label{t:model}}
%%\vspace{-7mm}
%\end{table}
%
%Our compartmentalized model induces specifications in %of interacting systems in 
%which   communication, runtime adaptation, and state (as in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns.
%%It is worth noticing that 
%Notice that
%the differences between %the syntax and semantics of 
%``plain'' processes 
%(as given in \S\,\ref{s:evadap}) and %those for 
%systems (as defined in Table~\ref{t:model}) are mostly conceptual, rather than technical. 
%In fact, the higher level of abstraction that is enforced by our model does not result in additional technicalities.
%%Although our compartmentalized model builds upon processes, w
%We conjecture that a reduction-preserving translation of application-based specifications into processes does not exist---a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. 
%This difference in terms of expressiveness does not appear to affect the type system. 
%%In fact, w
%In future work we plan to extend the 
%%We are confident that the 
%typing discipline in \S\,\ref{s:types} (and its associated safety and consistency guarantees) to systems. 
%%We plan to address this conjecture in future work.
%%For instance, typing the upgrades is simple using interfaces
%
%


\section{Related Work}\label{s:relw}
%\noindent\emph{\textbf{Related Work.}~}
%The closest related work is the PhD thesis of Kouzapas~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}, which introduces event-bases processes for asynchronous communication together with a complete framework to test arrival of messages and test types of queues. As mentioned throughout the paper we have been inspired by this machinery but we have considerably changed the domain and scope of application. 
% 
%\paragraph{\textbf{Related Work.}}

To the best of our knowledge our work develops the first application of 
constructs for 
type-directed checks and 
event-based communication for specifying and analyzing 
runtime adaptation for 
session-based concurrent systems.
In fact, although such constructs have been proposed in previous works,  
their application for runtime adaptation seems to be a new contribution of our work.
As such,  our work
develops an unexplored perspective for existing elements in session-based languages 
with the aim of enhancing the expressiveness of models and reasoning techniques for 
communication-centric systems which may be updated at runtime.


The combination of static typing and type-directed tests for dynamic reconfiguration is not new.
For instance, 
the work~\cite{DBLP:conf/esop/SecoC06} studies this combination 
in the very different setting of 
object-oriented component programming.
As already discussed, % along the paper, %the most related works are 
we build upon constructs proposed 
in~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}
for defining type-directed checks and expressing eventful sessions. 
The earliest works on eventful sessions, covering theory and implementation issues, are~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11}. %; an associated journal paper is~\cite{KouzapasJ13}. %We have often referred to 
Kouzapas's PhD thesis~\cite{Kouzapas12} provides a  unified presentation of the eventful session framework, with case studies including  event selectors (a building block in event-driven systems) and transformations between multithreaded and event-driven programs.  
%Besides the eventful process constructs, 
At the level of types, 
the work in~\cite{Kouzapas12} introduces session set types to support the $\mathtt{typecase}$ construct. 
%Since our typecase construct is embedded inside update processes, our type system may rely on a standard session type syntax.
In contrast, we use dynamic  type inspection only for runtime adaptation;  %, while 
in~\cite{Kouzapas12} 
$\mathtt{typecase}$ is part of the process syntax. 
This choice enables us 
to retain a standard session type syntax. %; see~\S\,\ref{s:types}. 
%As mentioned above, r

A number of previous works~\cite{GiustoP14short,DBLP:conf/aplas/AndersonR12,DBLP:conf/sefm/BravettiCHLMPZ13,CDV15j,DBLP:journals/corr/CastellaniDP14,DBLP:conf/sle/PredaGLMG14} have addressed forms of runtime adaptation for models of communicating systems based on binary and multiparty session types.
As we elaborate next, none of these works features the distinguishing constructs of our framework, namely adaptation routines based on type-directed checks on session types and eventful constructs for handling and triggering such routines. 

We have already mentioned how the present development was motivated as an enhancement to our previous work~\cite{GiustoP14short}, in which update processes do not consider type-directed checks and adaptation of located processes with open (running) sessions is disallowed by typing.
While~\cite{GiustoP14short} addresses binary session types, all of~\cite{DBLP:conf/aplas/AndersonR12,DBLP:conf/sefm/BravettiCHLMPZ13,CDV15j,DBLP:journals/corr/CastellaniDP14,DBLP:conf/sle/PredaGLMG14} concern 
models based on 
multiparty sessions and/or choreographies.
The work~\cite{DBLP:conf/aplas/AndersonR12} studies dynamic update for message passing programs; a form of consistency for updates over threads is ensured using multiparty session types, following an asynchronous communication discipline. 
The paper~\cite{DBLP:conf/sefm/BravettiCHLMPZ13} develops a model of choreography with interleaved sessions and 
adaptation as well as an associated endpoint language; choreographies and endpoints are related via projection, but typing is not addressed. The key ideas of the framework for self-adaptable multiparty sessions in~\cite{CDV15j} have been summarized in \S\,\ref{s:overv}. Our proposal for event-based adaptation for multiparty protocols, described in \S\,\ref{s:multi} departs from the approach in~\cite{CDV15j} and extends it to cover forms of unanticipated adaptation, including internal and external adaptation requests. Another work derived from~\cite{CDV15j} is~\cite{DBLP:journals/corr/CastellaniDP14} in which adaptation of multiparty protocols is coupled with mechanisms for enforcing secure information flow and access control. As such, it is both technically and conceptually  different from the proof of concept that we have described in \S\,\ref{s:multi}.   
Finally, the paper~\cite{DBLP:conf/sle/PredaGLMG14} describes a framework for programming distributed adaptive applications. The framework relies on a language for choreographies in which adaptation is specified following a rule-based approach. 





%\paragraph{\textbf{Concluding Remarks.}} 
%\noindent\emph{\textbf{Concluding Remarks.}~} 
\section{Concluding Remarks}\label{s:concl}
In this paper, we have introduced a novel approach to 
runtime adaptation of session typed processes;
the approach is based on two kinds of constructs: (i)~a process construct
for dynamic update
 based on type-directed checks and (ii)~on constructs for eventful sessions, namely queues equipped with an arrival predicate.
 The combination of these constructs allows us to specify dynamic modifications on the behavior of session-typed processes, therefore providing a basis for reasoning about expressive models of communication-centric systems with runtime adaptation.
In fact, these constructs allows us to specify  \emph{what} 
should be the content of an adaptation routine, but also 
\emph{when} it should be triggered.
The  constructs on which our approach relies are not new to this paper, but have been introduced and throughly studied by Kouzapas et al. in a series of works~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. 
Such works investigate foundational and practical issues for eventful binary sessions;
in our view, this adds significant value to our proposal, as 
the key syntactic elements on which it stands have been already validated (in theory and in practice) by previous independent studies.

Our study has addressed the case of structured protocols abstracted as binary session types; as a proof of concept for our approach, we have also explored the case of adaptation in multiparty sessions. 
The case of binary sessions represents a well-studied and representative setting, in which the distinguishing aspects of our approach can be introduced in a clean manner. 
We identified the strictly necessary eventful process constructs that enhance and refine the
mechanisms for runtime adaptation given in~\cite{GiustoP14short}. 
Adaptation requests, both internal and external, are handled via event detectors and queues associated to locations. 
Our approach enables us to 
specify rich forms of updates on locations with running sessions; this represents a concrete improvement with respect to~\cite{GiustoP14short}, in which updates are only allowed when locations do not enclose running sessions.
We notice that expressing both internal and external exceptional events is useful in practice; 
for instance, both kinds of events coexist in  
%the Business Process Model \& Notation (BPMN) 
BPMN 2.0~(see, e.g.,~\cite[Chap.4]{DBLP:books/daglib/0031128}).
To rule out update steps that jeopardize running session protocols, 
we also introduced a type system that ensures communication safety and update consistency for session programs.
%To further motivate   our  framework, 
Concerning our proof of concept for multiparty sessions, we described how our approach can be integrated on top of an recent proposal for self-adaptable multiparty sessions with asynchronous communication~\cite{CDV15j}. Also in this more general case we are able to specify internal and external adaptation requests, by relying on a model of interaction 
which organizes  communication and adaptation components into a sensible structure based on distributed locations. 


Directions for future work include validating our approach to adaptation in concrete case studios and different settings. 
For instance, we intend to 
revisit the model of \emph{supervision trees} (a mechanism for fault-tolerance in Erlang)
that we gave in~\cite{DBLP:journals/corr/GiustoP13}.
Also, it would be also interesting to explore if our approach based on events can be harmonized with the model of security-driven adaptation that we have developed in~\cite{DBLP:journals/corr/CastellaniDP14}, in which read and write violations to security policies determine events of a very specific nature. 


%Other interesting topics 
%for further development
%include accounting for 
%\emph{asynchronous} communication (cf. Remark~\ref{rem:asynch}) and 
%extending our event-based approach 
%to choreographic protocols; the framework in~\cite{CDV14} may provide a good starting point.

\paragraph{\textbf{Acknowledgments.}} 
%\noindent{\textbf{Acknowledgments.}} 
We are grateful to 
Ilaria Castellani, 
Mariangiola Dezani-Ciancaglini, 
%M. Dezani, 
and 
the anonymous reviewers for useful remarks and suggestions.
%The research reported in this paper 
This research was partially supported 
by a Short-Term Scientific Mission 
%STSM
grant to Di Giusto from 
COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems.
%(BETTY) -- \url{http://www.behavioural-types.eu}.

%\vspace{-2mm}

{%\small
\bibliographystyle{abbrv}
\bibliography{referen}
}

\input{appendix-fac}








\label{lastpage}

\end{document}
